LieIdealNormalityInput.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The published ideal-to-normal-subgroup implication

J. M. Lee, Introduction to Smooth Manifolds, second edition, GTM 218, Springer (2013), Theorem 20.28, pp.535–536 (Ideals and Normal Subgroups). https://doi.org/10.1007/978-1-4419-9982-5

Only the forward implication, for an embedded connected nilpotent subgroup, is retained. The actual differential is required to identify its Lie algebra with the given ideal. No ambient factorization or height assertion is assumed.

def OAI.PolycyclicRecognition.NilpotentIdealNormalityInput line 31
Source documentation
Exact connected embedded nilpotent specialization of Lee's ideal criterion. All Lie algebras here are the actual tangent Lie algebras.
```
def NilpotentIdealNormalityInput : Prop :=
…
```