OAI/GroupTheory/PolycyclicRecognition/Geometry/FiniteAssociativeBCH.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite BCH in an associative algebra with vanishing long products

The universal logarithm constructs the finite Baker--Campbell--Hausdorff coefficients.

  1. def OAI.PolycyclicRecognition.finiteUniversalLiePolynomial line 19
  2. theorem OAI.PolycyclicRecognition.rationalUniversalLogarithm_eval_lie line 27
  3. theorem OAI.PolycyclicRecognition.finite_associative_bch line 40

    Source documentation

    A finite, universal right-nested Lie polynomial gives the exponential product.

    theorem finite_associative_bch :
    (List.ofFn (fun i => IsNilpotent.exp (X i))).prod =
      IsNilpotent.exp (finiteUniversalLiePolynomial (c := c) X) := by
…

    Mentions: OAI.PolycyclicRecognition.finiteUniversalLiePolynomial

  4. theorem OAI.PolycyclicRecognition.finiteUniversalLiePolynomial_pow line 53