OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentByAbelianSplitRealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Realizing split nilpotent-by-free-abelian groups as virtual Lie lattices

  1. theorem OAI.PolycyclicRecognition.nilpotent_by_freeAbelian_split_uniform_lattice line 13