PolynomialSubalgebraCoordinates.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Smooth polynomial coordinates on an inherited nilpotent subgroup

Intrinsic integration identifies the independently constructed BCH law with the ambient group's restricted law. This retains the actual embedded subgroup.

def OAI.PolycyclicRecognition.normedLieSubalgebra line 19
theorem OAI.PolycyclicRecognition.polynomialSubalgebra_intrinsic_mul line 27
Source documentation
Any intrinsic polynomial model on a Lie subalgebra has the inherited product.
```
theorem polynomialSubalgebra_intrinsic_mul (K : LieSubalgebra ℝ L)
    (hnil : LieRing.IsNilpotent K) :
    letI := normedLieSubalgebra K
…
```
Mentions: OAI.PolycyclicRecognition.normedLieSubalgebra
theorem OAI.PolycyclicRecognition.polynomialSubalgebra_intrinsic_group line 49
theorem OAI.PolycyclicRecognition.polynomialSubalgebra_coordinates line 60
Source documentation
The inherited group itself admits polynomial exponential coordinates.
```
theorem polynomialSubalgebra_coordinates (K : LieSubalgebra ℝ L)
    (hnil : LieRing.IsNilpotent K) :
    letI := normedLieSubalgebra K
…
```
Mentions: OAI.PolycyclicRecognition.normedLieSubalgebra
theorem OAI.PolycyclicRecognition.polynomialSubalgebra_lieGroup line 69
Source documentation
The topology and inherited multiplication form the same smooth Lie group.
```
theorem polynomialSubalgebra_lieGroup (K : LieSubalgebra ℝ L)
    (hnil : LieRing.IsNilpotent K) :
    letI := normedLieSubalgebra K
…
```
Mentions: OAI.PolycyclicRecognition.normedLieSubalgebra