OAI/Combinatorics/Progressions/Nilpotent/PolynomialShearBCH.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.polynomialShearAssociativeAction line 16
  2. theorem OAI.Erdos3.polynomialShearAssociativeAction_positive line 35
  3. theorem OAI.Erdos3.polynomialShearExpOn_lieBCH line 40
  4. theorem OAI.Erdos3.polynomialShearExpAut_lieBCH line 57
  5. def OAI.Erdos3.polynomialShearBCHEquiv line 69
  6. theorem OAI.Erdos3.weightedLoweringAut_isNilpotent line 77
  7. theorem OAI.Erdos3.weightedLoweringAut_nilpotencyClass_le line 82