OAI/GroupTheory/PolycyclicRecognition/Algebra/DynkinTranslations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual inverse of a coordinate right translation

  1. def OAI.PolycyclicRecognition.dynkinRightTranslation line 15

    Source documentation

    The finite group laws give a homeomorphism, with inverse translation parameter -q. This identifies the inverse used by sampling densities.

    def dynkinRightTranslation {c : ℕ} (a : DynkinCoefficients c 2)
    (B : V →L[ℝ] V →L[ℝ] V) (h : PolynomialGroupLaws (dynkinProduct a B))
    (q : V) : V ≃ₜ V where
…

    Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct

  2. theorem OAI.PolycyclicRecognition.dynkinRightTranslation_apply line 34
  3. theorem OAI.PolycyclicRecognition.dynkinRightTranslation_symm_apply line 38