OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianDynkinInput.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite BCH for commutative Lie groups

  1. theorem OAI.PolycyclicRecognition.IsGroupExponential.map_add_of_comm line 18
  2. theorem OAI.PolycyclicRecognition.IsGroupExponential.prod_eq_exp_sum_of_comm line 41
  3. def OAI.PolycyclicRecognition.abelianDynkinCoefficients line 51

    Source documentation

    Only the degree-one coefficients are nonzero.

    def abelianDynkinCoefficients (c n : ℕ) : DynkinCoefficients c n :=
…

    Mentions: OAI.PolycyclicRecognition.DynkinCoefficients

  4. theorem OAI.PolycyclicRecognition.abelianDynkinCoefficients_bound line 54
  5. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_abelian line 63
  6. theorem OAI.PolycyclicRecognition.nilpotentDynkinExpansionInput_of_comm line 77

    Source documentation

    The published BCH input is fully proved for commutative Lie groups.

    theorem nilpotentDynkinExpansionInput_of_comm [FiniteDimensional ℝ E] :
    NilpotentDynkinExpansionInput E G := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput