OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanPublishedOffsetThreshold.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform offsets from published finite-cone realization inputs

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_published_polar_offset_threshold line 48

    Source documentation

    Construct the finite cone models before taking the common offset threshold. No target model, Haar action or trace comparison is assumed.

    theorem exists_published_polar_offset_threshold
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput