OAI/NumberTheory/DukePrimeDegree/Geometry/NeutralUpperRootChart.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Move the neutral coordinate to the right of the root coordinate

The parametrization is now lower-unitriangular, upper-unipotent, diagonal. Consequently right translation by the diagonal group is translation in the last coordinate, with the other two coordinates fixed.

  1. theorem OAI.DukePrimeDegree.EliminationChain.continuous_rootDilation line 20
  2. def OAI.DukePrimeDegree.neutralUpperRootParam line 38
  3. lemma OAI.DukePrimeDegree.neutralUpperRootParam_eq line 43
  4. lemma OAI.DukePrimeDegree.continuous_neutralUpperRootParam line 58
  5. lemma OAI.DukePrimeDegree.neutralUpperRootParam_translate line 84