OAI/NumberTheory/DukePrimeDegree/Dynamics/ShearingReturnGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Relative matrices after diagonal and root translation

These identities track the right-action convention in the return-pair argument. After simultaneous root translation by t, the relative matrix is conjugated by the root element at -t.

  1. lemma OAI.DukePrimeDegree.rootPairConjugate_rightAction line 19
  2. lemma OAI.DukePrimeDegree.rootConjugate_rightAction line 26