OAI/Geometry/HeilbronnTriangle/RowLatticeFixedDet.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem355.RowLatticeFixedDet.IntMatrix line 15
2. theorem OAI.Problem355.RowLatticeFixedDet.card_le_of_anisotropic line 17
3. theorem OAI.Problem355.RowLatticeFixedDet.orbit_card_le_of_anisotropic line 33
4. theorem OAI.Problem355.RowLatticeFixedDet.prime_power_card_le_of_anisotropic line 47
5. theorem OAI.Problem355.RowLatticeFixedDet.card_le line 65
6. theorem OAI.Problem355.RowLatticeFixedDet.orbit_card_le line 77
7. theorem OAI.Problem355.RowLatticeFixedDet.prime_power_card_le line 90