OAI/GroupTheory/PolycyclicRecognition/Algebra/FaithfulGroupDynkin.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite BCH for faithfully represented Lie groups

The target representation need not have nilpotent operators. Instead, the constructed nilpotent coordinate model maps to the target by the proved integration theorem. Its exact class-bounded product formula then descends.

  1. theorem OAI.PolycyclicRecognition.nilpotentDynkinExpansionInput_of_faithful line 24