OAI/NumberTheory/DukePrimeDegree/Geometry/RootCommutator.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The three-root commutator rectangle

The two orders of the adjacent root translations differ by the product of their parameters in the long root. Under a diagonal flow neutral on the long root and contracting the first root, this is the exact limit.

  1. lemma OAI.DukePrimeDegree.adjacent_root_conjugation line 21
  2. theorem OAI.DukePrimeDegree.adjacent_root_conjugate_limit line 44