OAI/GroupTheory/PolycyclicRecognition/Lattices/TwoStepFiniteIndexRealization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite-index lattice realization for two-step nilpotent groups

  1. theorem OAI.PolycyclicRecognition.commutator_le_center_of_injective line 11
  2. theorem OAI.PolycyclicRecognition.twoStep_finiteIndex_lattice_realization line 25