OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialCommutingProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Products of commuting logarithms

The finite BCH law is addition when the two logarithms have zero bracket.

  1. theorem OAI.PolycyclicRecognition.polynomial_mul_eq_add_of_lie_eq_zero line 16
  2. theorem OAI.PolycyclicRecognition.polynomial_mem_center_of_lie_eq_zero line 47