OAI/GroupTheory/PolycyclicRecognition/Analysis/ProbePivotBridge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.probe_pivot_bridge_identity line 12
2. theorem OAI.PolycyclicRecognition.probe_pivot_bridge_distance line 29

   Source documentation

   The common ideal probe and basepoint disappear from the bridge length.

   theorem probe_pivot_bridge_distance
       (φ : D →* MulAut N) (ι : N →* G) (κ : D →* G)
       (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
       (S : MulAut N) (n i s k : N) (d : D) (x : G) :
       dist (x * (ι (coneProbeFirst S n i s) * κ d))
         (x * (ι (coneProbeSecond S n i k) * κ d)) =
           dist 1 (ι (φ d⁻¹ (S (s⁻¹ * k)))) := by
   …

   Mentions: OAI.PolycyclicRecognition.coneProbeFirst, OAI.PolycyclicRecognition.coneProbeSecond