OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentCyclicKernelCompletion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing a nilpotent group across an actual cyclic quotient

  1. theorem OAI.PolycyclicRecognition.nilpotent_cyclic_kernel_completion_with_dimension line 16
  2. theorem OAI.PolycyclicRecognition.nilpotent_cyclic_kernel_completion line 38