OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentIntegralKernelCompletion.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Completing every nilpotent extension of a real kernel by an integral lattice

The quotient rank induction removes an actual coordinate, completes its kernel, and constructs the next real cyclic direction. The section relations and all maps are retained through the group isomorphisms.

  1. theorem OAI.PolycyclicRecognition.nilpotent_integral_kernel_completion_with_dimension line 20
  2. theorem OAI.PolycyclicRecognition.nilpotent_integral_kernel_completion line 75