OAI/Combinatorics/KMedian/Compression/AffineElimination.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedian.IntegerLaw line 9
2. def OAI.MetricKMedian.IntegerLaw.rational line 19
3. theorem OAI.MetricKMedian.IntegerLaw.numerator_le line 25
4. theorem OAI.MetricKMedian.IntegerLaw.positive_entry line 29
5. theorem OAI.MetricKMedian.IntegerLaw.eliminate line 46
6. theorem OAI.MetricKMedian.IntegerLaw.denominator_step_bound line 113