OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootDilation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Diagonal dynamics in ordered upper-root coordinates

Conjugation by a diagonal element is exactly the product of the root coordinate dilations, with each factor carrying its own root weight.

  1. def OAI.DukePrimeDegree.EliminationChain.rootDilation line 21
  2. theorem OAI.DukePrimeDegree.EliminationChain.word_rootDilation line 28
  3. theorem OAI.DukePrimeDegree.upperRootWord_diagonal line 49
  4. theorem OAI.DukePrimeDegree.upperRoot_orbit_diagonal line 56