OAI/Geometry/HeilbronnTriangle/LatticeResidues.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem355.LatticeResidues.eq_of_ediv_eq_of_emod_eq line 10
2. theorem OAI.Problem355.LatticeResidues.card_residue_interval_le line 17
3. theorem OAI.Problem355.LatticeResidues.card_residue_box_le line 37
4. theorem OAI.Problem355.LatticeResidues.card_residue_cube_le line 61
5. theorem OAI.Problem355.LatticeResidues.card_residue_classes_cube_le line 67
6. theorem OAI.Problem355.LatticeResidues.symmetric_quotient_bound line 85
7. theorem OAI.Problem355.LatticeResidues.card_symmetric_residue_classes_le line 93
8. theorem OAI.Problem355.LatticeResidues.card_symmetric_residue_classes_mul_pow_le line 101
9. theorem OAI.Problem355.LatticeResidues.card_thin_residue_classes_mul_sq_le line 122
10. theorem OAI.Problem355.LatticeResidues.card_modular_line_mul_sq_le line 137