OAI/Geometry/NilpotentCharts/Coordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Rational triangular coordinates, second-kind axes and lattice chart structures.

  1. structure OAI.RationalLattice.RealCoordinates line 13
  2. def OAI.MalcevCharacters.axis line 29
  3. structure OAI.MalcevCharacters.SecondKind line 31
  4. structure OAI.CubeFaces.Filtration line 38
  5. structure OAI.SourceProductChart.Chart line 46
  6. def OAI.SourceRawChartGap.RawChartExists line 68
  7. def OAI.RationalLattice.IsPolyCoord line 83
  8. lemma OAI.RationalLattice.isPoly_correction line 85
  9. lemma OAI.RationalLattice.IsPolyCoord.const line 91
  10. lemma OAI.RationalLattice.IsPolyCoord.mul line 93
  11. lemma OAI.RationalLattice.IsPolyCoord.inv line 102
  12. lemma OAI.RationalLattice.IsPolyCoord.bracket line 126