OAI/GroupTheory/PolycyclicRecognition/Geometry/FaithfulRepresentationBCH.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Transporting finite BCH through an actual faithful group representation

The derivative is the Lie homomorphism used in the polynomial. The only algebraic assumption is a concrete common bound on products of its values.

  1. theorem OAI.PolycyclicRecognition.finite_bch_of_faithful_nilpotent_representation line 24