OAI/Geometry/HeilbronnTriangle/IntegralPlaneLattice.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem355.IntegralPlaneLattice.Ambient line 12
  2. def OAI.Problem355.IntegralPlaneLattice.stdBasis line 14
  3. def OAI.Problem355.IntegralPlaneLattice.standardLattice line 16
  4. instance OAI.Problem355.IntegralPlaneLattice.(instance at line 18) line 18
  5. def OAI.Problem355.IntegralPlaneLattice.castVec line 22
  6. lemma OAI.Problem355.IntegralPlaneLattice.castVec_apply line 24
  7. lemma OAI.Problem355.IntegralPlaneLattice.stdBasis_repr line 26
  8. lemma OAI.Problem355.IntegralPlaneLattice.mem_standardLattice line 28
  9. lemma OAI.Problem355.IntegralPlaneLattice.castVec_mem line 34
  10. def OAI.Problem355.IntegralPlaneLattice.realDot line 37
  11. lemma OAI.Problem355.IntegralPlaneLattice.realDot_apply line 42
  12. lemma OAI.Problem355.IntegralPlaneLattice.realDot_castVec line 45
  13. def OAI.Problem355.IntegralPlaneLattice.plane line 49
  14. def OAI.Problem355.IntegralPlaneLattice.lattice line 51
  15. instance OAI.Problem355.IntegralPlaneLattice.lattice_discrete line 54
  16. lemma OAI.Problem355.IntegralPlaneLattice.realDot_stdBasis line 60
  17. def OAI.Problem355.IntegralPlaneLattice.projection line 63
  18. lemma OAI.Problem355.IntegralPlaneLattice.projection_apply line 70
  19. lemma OAI.Problem355.IntegralPlaneLattice.projection_on_plane line 73
  20. lemma OAI.Problem355.IntegralPlaneLattice.projection_basis_mem line 80
  21. lemma OAI.Problem355.IntegralPlaneLattice.lattice_spans line 89
  22. lemma OAI.Problem355.IntegralPlaneLattice.isZLattice line 99
  23. lemma OAI.Problem355.IntegralPlaneLattice.plane_finrank line 102
  24. lemma OAI.Problem355.IntegralPlaneLattice.lattice_finrank line 115
  25. def OAI.Problem355.IntegralPlaneLattice.basis line 120
  26. def OAI.Problem355.IntegralPlaneLattice.integerDot line 124
  27. def OAI.Problem355.IntegralPlaneLattice.integerPlane line 129
  28. def OAI.Problem355.IntegralPlaneLattice.kernelMap line 131
  29. lemma OAI.Problem355.IntegralPlaneLattice.kernelMap_injective line 148
  30. lemma OAI.Problem355.IntegralPlaneLattice.kernelMap_surjective line 156
  31. def OAI.Problem355.IntegralPlaneLattice.kernelEquiv line 173
  32. def OAI.Problem355.IntegralPlaneLattice.integerBasis line 176
  33. def OAI.Problem355.IntegralPlaneLattice.castLinear line 179
  34. def OAI.Problem355.IntegralPlaneLattice.realLattice line 184
  35. lemma OAI.Problem355.IntegralPlaneLattice.realLattice_le_standard line 186
  36. instance OAI.Problem355.IntegralPlaneLattice.realLattice_discrete line 191
  37. def OAI.Problem355.IntegralPlaneLattice.latticeIn line 196
  38. instance OAI.Problem355.IntegralPlaneLattice.latticeIn_discrete line 199
  39. lemma OAI.Problem355.IntegralPlaneLattice.latticeIn_spans line 206
  40. lemma OAI.Problem355.IntegralPlaneLattice.latticeIn_isZLattice line 227
  41. lemma OAI.Problem355.IntegralPlaneLattice.latticeIn_finrank line 232
  42. def OAI.Problem355.IntegralPlaneLattice.basisIn line 238
  43. def OAI.Problem355.IntegralPlaneLattice.integerPlaneIn line 245
  44. def OAI.Problem355.IntegralPlaneLattice.kernelMapIn line 248
  45. lemma OAI.Problem355.IntegralPlaneLattice.kernelMapIn_injective line 266
  46. lemma OAI.Problem355.IntegralPlaneLattice.kernelMapIn_surjective line 275
  47. def OAI.Problem355.IntegralPlaneLattice.kernelEquivIn line 290
  48. def OAI.Problem355.IntegralPlaneLattice.integerBasisIn line 295
  49. lemma OAI.Problem355.IntegralPlaneLattice.cast_integerBasisIn line 301