OAI/Combinatorics/KMedian/Binary/BinaryNatural.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Binary.Word.normalize_length line 14
  2. theorem OAI.MetricKMedian.Binary.Word.bits_value_length line 17
  3. theorem OAI.MetricKMedian.Binary.NatBinary.zero_iff line 23
  4. theorem OAI.MetricKMedian.Binary.NatBinary.bit_length line 31
  5. theorem OAI.MetricKMedian.Binary.NatBinary.half_length line 35
  6. theorem OAI.MetricKMedian.Binary.NatBinary.add_length line 38
  7. theorem OAI.MetricKMedian.Binary.NatBinary.mul_length line 46
  8. theorem OAI.MetricKMedian.Binary.NatBinary.length_mono line 54
  9. theorem OAI.MetricKMedian.Binary.NatBinary.half_lt_length line 57
  10. def OAI.MetricKMedian.Binary.PolyProgram.natBit line 65
  11. def OAI.MetricKMedian.Binary.PolyProgram.natHalf line 69
  12. def OAI.MetricKMedian.Binary.PolyProgram.natOdd line 72
  13. def OAI.MetricKMedian.Binary.PolyProgram.natZero line 77