OAI/Geometry/HeilbronnTriangle/RowLattice.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.RowLattice.RowKernel line 15
  2. def OAI.Problem355.RowLattice.rowImage line 18
  3. lemma OAI.Problem355.RowLattice.rowImage_index_eq_card_kernel line 21
  4. def OAI.Problem355.RowLattice.diagonalKernelEquiv line 25
  5. lemma OAI.Problem355.RowLattice.card_diagonal_kernel line 51
  6. def OAI.Problem355.RowLattice.kernelEquivOfDiagonalForm line 55
  7. lemma OAI.Problem355.RowLattice.rowImage_index_of_diagonal_form line 78
  8. def OAI.Problem355.RowLattice.reduction line 87
  9. lemma OAI.Problem355.RowLattice.reduction_surjective line 92
  10. def OAI.Problem355.RowLattice.integerRowLattice line 97
  11. lemma OAI.Problem355.RowLattice.integerRowLattice_index line 101
  12. theorem OAI.Problem355.RowLattice.integerRowLattice_index_prime_power line 105
  13. lemma OAI.Problem355.RowLattice.smul_mem_rowImage_diagonal line 119
  14. lemma OAI.Problem355.RowLattice.smul_mem_rowImage_of_diagonal_form line 127
  15. lemma OAI.Problem355.RowLattice.rowImage_eq_rowSpan line 144
  16. theorem OAI.Problem355.RowLattice.nsmul_mem_integerRowLattice_prime_power line 148
  17. instance OAI.Problem355.RowLattice.integerRowLattice_finiteIndex line 167
  18. theorem OAI.Problem355.RowLattice.integerRowLattice_finrank line 173
  19. lemma OAI.Problem355.RowLattice.rowImage_left_unit line 178
  20. lemma OAI.Problem355.RowLattice.row_mem_integerRowLattice_of_reduction_eq line 194