OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialSubalgebraFiltration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Intrinsic lower-central estimates on polynomial Lie subgroups

The restricted BCH law has the same normalized linear term. Its higher terms raise the intrinsic lower central series of the subalgebra.

  1. theorem OAI.PolycyclicRecognition.polynomialSubalgebra_axis_normalized line 19
  2. theorem OAI.PolycyclicRecognition.polynomialSubalgebra_mul_difference line 31
  3. theorem OAI.PolycyclicRecognition.polynomialSubalgebra_inner_difference line 49