OAI/GroupTheory/PolycyclicRecognition/Geometry/IntrinsicCartanFactorModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Cartan factors from the intrinsic height kernel

Both nilpotent factor inclusions are closed without the ambient exponential chart. Their product and exact overlap follow from local multiplication coordinates and uniqueness of exponential preimages in the height kernel.

  1. theorem OAI.PolycyclicRecognition.nonempty_intrinsic_cartanFactorModel line 34