OAI/Geometry/HeilbronnTriangle/PrimePowerRowData.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem355.PrimePowerRowData.integerLift line 14
  2. theorem OAI.Problem355.PrimePowerRowData.integerLift_reduction line 18
  3. abbrev OAI.Problem355.PrimePowerRowData.rowModule line 24
  4. theorem OAI.Problem355.PrimePowerRowData.integerLift_row_mem line 30
  5. theorem OAI.Problem355.PrimePowerRowData.integerLift_diagonalization line 36
  6. theorem OAI.Problem355.PrimePowerRowData.rowModule_index line 45
  7. theorem OAI.Problem355.PrimePowerRowData.larger_divisor_nsmul_mem line 50
  8. theorem OAI.Problem355.PrimePowerRowData.larger_divisor_zsmul_mem line 54
  9. theorem OAI.Problem355.PrimePowerRowData.larger_divisor_isUnit line 58
  10. theorem OAI.Problem355.PrimePowerRowData.pairing_pos_and_dvd line 65
  11. theorem OAI.Problem355.PrimePowerRowData.pairing_cube_le line 73
  12. theorem OAI.Problem355.PrimePowerRowData.plane_covolume line 87
  13. theorem OAI.Problem355.PrimePowerRowData.orbit_rows_mem line 98