OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPublishedPolarAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polar quotient actions from the precise published realization

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.MeasuredCone.polar_action_haar_of_published_realization line 36

    Source documentation

    The published faithful exponential realization constructs the actual polar quotient action and its Haar multiplier for the already constructed cone model. It contributes no metric or chosen-height compatibility.

    theorem MeasuredCone.polar_action_haar_of_published_realization
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput