OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootEuclideanCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

One real coordinate for each positive root

The elimination time space is canonically a finite product of real lines, indexed without repetition by the positive roots. Diagonal conjugation scales each coordinate by its own root character.

  1. def OAI.DukePrimeDegree.realVectorConsHomeomorph line 22
  2. def OAI.DukePrimeDegree.EliminationChain.timeVectorHomeomorph line 33
  3. lemma OAI.DukePrimeDegree.EliminationChain.timeVectorHomeomorph_cube line 40
  4. lemma OAI.DukePrimeDegree.EliminationChain.timeVectorHomeomorph_dilation line 59
  5. def OAI.DukePrimeDegree.upperRootIndexEquiv line 82
  6. def OAI.DukePrimeDegree.realCoordinatesReindex line 90
  7. def OAI.DukePrimeDegree.upperRootEuclideanCoordinates line 98
  8. lemma OAI.DukePrimeDegree.upperRootIndexEquiv_val line 102
  9. lemma OAI.DukePrimeDegree.upperRootEuclideanCoordinates_cube line 105
  10. lemma OAI.DukePrimeDegree.upperRootEuclideanCoordinates_dilation line 117