OAI/Geometry/HeilbronnTriangle/PrimePowerData.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Problem355.PrimePowerData line 12
  2. theorem OAI.Problem355.PrimePowerData.nonempty_of_unit line 27
  3. def OAI.Problem355.PrimePowerData.ofUnit line 46
  4. lemma OAI.Problem355.PrimePowerData.b_le_k line 50
  5. theorem OAI.Problem355.PrimePowerData.row_lattice_index line 53
  6. theorem OAI.Problem355.PrimePowerData.multiple_mem_row_lattice line 60
  7. theorem OAI.Problem355.PrimePowerData.orbit_lower_bound line 66
  8. theorem OAI.Problem355.PrimePowerData.minors_vanish_iff line 73
  9. theorem OAI.Problem355.PrimePowerData.b_unique line 80
  10. theorem OAI.Problem355.PrimePowerData.e_unique line 87