OAI/GroupTheory/PolycyclicRecognition/Lattices/KernelCompletionUnipotentLift.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nilpotent ambient conjugations extend as unipotent Lie automorphisms

  1. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.unipotent_conjugation_extension line 17