OAI/Geometry/HeilbronnTriangle/IntegralPlaneReduction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.IntegralPlaneReduction.Vector line 11
  2. def OAI.Problem355.IntegralPlaneReduction.integralNormal line 13
  3. def OAI.Problem355.IntegralPlaneReduction.integralPlane line 15
  4. def OAI.Problem355.IntegralPlaneReduction.reducedNormal line 18
  5. theorem OAI.Problem355.IntegralPlaneReduction.mem_integralPlane line 20
  6. def OAI.Problem355.IntegralPlaneReduction.reductionHom line 23
  7. theorem OAI.Problem355.IntegralPlaneReduction.reductionHom_apply line 32
  8. theorem OAI.Problem355.IntegralPlaneReduction.reductionHom_surjective line 37
  9. theorem OAI.Problem355.IntegralPlaneReduction.reducedNormal_ne_zero line 48
  10. def OAI.Problem355.IntegralPlaneReduction.lineLattice line 54
  11. theorem OAI.Problem355.IntegralPlaneReduction.lineLattice_index line 59
  12. theorem OAI.Problem355.IntegralPlaneReduction.card_lines line 69
  13. theorem OAI.Problem355.IntegralPlaneReduction.equalCoordinate_index line 74