OAI/Geometry/HeilbronnTriangle/FixedDetLattice.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.FixedDetLattice.E line 14
  2. def OAI.Problem355.FixedDetLattice.basisMatrix line 16
  3. lemma OAI.Problem355.FixedDetLattice.orthonormal_det_eq line 19
  4. lemma OAI.Problem355.FixedDetLattice.covolume_span_basis_eq_det line 28
  5. lemma OAI.Problem355.FixedDetLattice.basisMatrix_det_ne_zero line 37
  6. lemma OAI.Problem355.FixedDetLattice.basisMatrix_coord_bound line 42
  7. lemma OAI.Problem355.FixedDetLattice.relIndex_clears_rows line 46
  8. theorem OAI.Problem355.FixedDetLattice.fixed_det_count_of_successive_basis line 61
  9. lemma OAI.Problem355.FixedDetLattice.last_norm_le_of_matrix line 120
  10. theorem OAI.Problem355.FixedDetLattice.fixed_det_count line 150
  11. theorem OAI.Problem355.FixedDetLattice.integer_fixed_det_count line 179