OAI/GroupTheory/PolycyclicRecognition/Algebra/UnipotentExtensionNilpotence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nilpotence from unipotent quotient generators

This applies the proved lower-central-layer argument to the entire kernel: the auxiliary fixed family consists only of the identity operator.

  1. theorem OAI.PolycyclicRecognition.extension_nilpotent_of_unipotent_generators line 19