OAI/GroupTheory/PolycyclicRecognition/Geometry/ClosedIntegrationOverHeight.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Closed nilpotent integration over the canonical height quotient

A nilpotent subalgebra projecting onto height has a closed integrated image. The proof compares its kernel with the constructed nilpotent height kernel and uses section coordinates for the remaining directions.

  1. theorem OAI.PolycyclicRecognition.exists_closed_nilpotent_integration_over_height line 31