OAI/Geometry/HeilbronnTriangle/PlaneBasisIndex.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.LatticeSplit.twoPlusOneEquiv line 11
  2. theorem OAI.Problem355.LatticeSplit.twoPlusOneEquiv_symm_zero line 22
  3. theorem OAI.Problem355.LatticeSplit.twoPlusOneEquiv_symm_one line 23
  4. theorem OAI.Problem355.LatticeSplit.twoPlusOneEquiv_symm_two line 24
  5. def OAI.Problem355.LatticeSplit.extendIntegerKernelBasis3 line 28
  6. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis3_zero line 33
  7. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis3_one line 39
  8. theorem OAI.Problem355.LatticeSplit.extendIntegerKernelBasis3_two line 45
  9. theorem OAI.Problem355.LatticeSplit.index_eq_natAbs_det_basis line 51
  10. theorem OAI.Problem355.LatticeSplit.abs_det_real_basis_eq_index line 58
  11. theorem OAI.Problem355.LatticeSplit.abs_det_kernel_height_eq_index line 64
  12. theorem OAI.Problem355.LatticeSplit.abs_det_real_full_basis_eq_one line 76
  13. theorem OAI.Problem355.LatticeSplit.abs_det_primitive_kernel_height_eq_one line 88