OAI/GroupTheory/PolycyclicRecognition/Lattices/KernelCompletionCyclicStep.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A cyclic step in completing a nilpotent extension with a real kernel

This constructs the next polynomial model, its faithful embedding, its integer grid and its homomorphism extension property. No lattice in the kernel is required.

  1. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.cyclic_step_with_dimension line 23
  2. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.cyclic_step line 110