OAI/GroupTheory/PolycyclicRecognition/Algebra/ClosedIntegrationOverLinearQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Closed nilpotent integration over a real linear quotient

This is the section-and-kernel argument with the concrete kernel supplied explicitly. It applies to the complex adjoint-weight quotient, regarded as a real vector space, without real triangularity of the original group.

  1. theorem OAI.PolycyclicRecognition.exists_closed_nilpotent_integration_over_linear_quotient line 25