OAI/Combinatorics/KMedian/Binary/BinaryFloor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Binary.Automatic.Poly.int_natAbs line 10
2. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_num line 12
3. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_den line 14
4. theorem OAI.MetricKMedian.Binary.Automatic.Poly.natFloor_eq line 16
5. theorem OAI.MetricKMedian.Binary.Automatic.Poly.rat_floor line 26