OAI/Geometry/HeilbronnTriangle/OrbitRowLattice.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem355.OrbitRowLattice.rowImage_mul_left_unit line 13
  2. theorem OAI.Problem355.OrbitRowLattice.rowImage_eq_of_mem_slOrbit line 32
  3. theorem OAI.Problem355.OrbitRowLattice.row_mem_rowImage line 38
  4. theorem OAI.Problem355.OrbitRowLattice.row_mem_integerRowLattice_of_reduction_mem_slOrbit line 44
  5. theorem OAI.Problem355.OrbitRowLattice.det_eq_of_mem_slOrbit line 53
  6. theorem OAI.Problem355.OrbitRowLattice.det_cast_eq_of_reduction_mem_slOrbit line 59
  7. theorem OAI.Problem355.OrbitRowLattice.small_representative_unique line 69
  8. theorem OAI.Problem355.OrbitRowLattice.small_determinants_unique line 79