OAI/GroupTheory/PolycyclicRecognition/Geometry/RotationalTwistConjugation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.rotationalTwistLift_conjugation_left line 20

   Source documentation

   The graph conjugation is the original conjugation followed by the inverse compact rotation.

   theorem rotationalTwistLift_conjugation_left (d : D) (n : N)
       (hn : τ (iN n) = 1) :
       ((rotationalTwistLift α τ hinv iD hD d *
         rotationalTwistLift α τ hinv iN hN n *
         (rotationalTwistLift α τ hinv iD hD d)⁻¹).val.left) =
         α ((τ (iD d))⁻¹) (iD d * iN n * (iD d)⁻¹) := by
   …

   Mentions: OAI.PolycyclicRecognition.rotationalTwistLift