OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGoodFacetAgreement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Contact-facet equality for the diagonal's nonempty good sheets

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.good_word_profiles_agree_on_facet line 26

    Source documentation

    At a facet, even good sets of vanishing relative mass force equality of the two limiting affine values. Their nonemptiness suffices for this step.

    theorem good_word_profiles_agree_on_facet
    (Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G) (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput