OAI/Geometry/HeilbronnTriangle/DeterminantResidue.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem355.DeterminantResidue.small_eq_of_modEq line 7
2. lemma OAI.Problem355.DeterminantResidue.small_eq_of_zmod_eq line 17
3. lemma OAI.Problem355.DeterminantResidue.small_residue_subsingleton line 21
4. lemma OAI.Problem355.DeterminantResidue.small_filter_eq_fiber line 26
5. lemma OAI.Problem355.DeterminantResidue.sum_small_le_of_fiber_bound line 40
6. lemma OAI.Problem355.DeterminantResidue.cast_det line 57
7. lemma OAI.Problem355.DeterminantResidue.det_residue_of_specialLinear line 61
8. lemma OAI.Problem355.DeterminantResidue.small_determinants_eq_of_same_orbit line 67
9. lemma OAI.Problem355.DeterminantResidue.cast_det_ne_zero_of_abs_lt line 78
10. lemma OAI.Problem355.DeterminantResidue.affineIndependent_cols_mod_of_small_nonzero_det line 84
11. lemma OAI.Problem355.DeterminantResidue.sum_small_determinants_le line 92
12. lemma OAI.Problem355.DeterminantResidue.sum_nonzero_det_weights_le line 105