OAI/GroupTheory/PolycyclicRecognition/Geometry/BasisAdjointNilpotent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A uniform nilpotence exponent for every coordinate adjoint

  1. theorem OAI.PolycyclicRecognition.basisBracket_pow_eq_zero line 14

    Source documentation

    Coordinate adjoints are uniformly nilpotent at any index at which the actual lower central series vanishes.

    theorem basisBracket_pow_eq_zero
    {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n k : ℕ}
    (b : Basis (Fin n) ℝ L) (hk : lowerCentralSeries ℝ L L k = ⊥)
    (x : Fin n → ℝ) : (basisBracket b x) ^ k = 0 := by
…

    Mentions: OAI.PolycyclicRecognition.basisBracket