OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborProfileAffinity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_supported_neighbor_profiles_affine_sequence line 35

   Source documentation

   Every supported neighboring pair is affine on the contracted profile domain, using the exact two marginal cell laws. The labels are not assumed to agree here; their equality is the shrinking-diagonal theorem.

   theorem cartan_supported_neighbor_profiles_affine_sequence
       [IsTopologicalGroup F.N.carrier]
       [Nonempty (Fin (finrank ℝ (cartanRootIdeal H)))]
       (hExp : IsGroupExponential Exp)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput