Theorems · Definition · nonassociative algebras
LieRing.IsNilpotent
(L : Type v) → [LieRing L] → Prop
We say a Lie ring is nilpotent when it is nilpotent as a Lie module over itself via the adjoint representation.
- Defined in
- Mathlib.Algebra.Lie.Nilpotent
- Cited by
- 176 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 36 definitions · uses no axioms
- Assumes
- LieRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LieRingstatement and proof · cited by 1,548
- LieModule.IsNilpotentproof · cited by 46
Cited by212
Results whose statement or proof uses this declaration.
- LieModule.Weightstatement · cited by 172
- LieModule.genWeightSpacestatement and proof · cited by 99
- LieAlgebra.rootSpacestatement and proof · cited by 74
- LieModule.Weight.IsNonZerostatement and proof · cited by 47
- LieModule.Weight.toLinearstatement and proof · cited by 41
- LieModule.Weight.IsZerostatement and proof · cited by 31
- LieModule.chainTopCoeffstatement and proof · cited by 30
- LieAlgebra.corootSpacestatement and proof · cited by 23
- LieModule.chainBotCoeffstatement and proof · cited by 22
- LieModule.chainTopstatement and proof · cited by 20
- LieModule.LinearWeightsstatement · cited by 19
- LieModule.genWeightSpaceOfstatement and proof · cited by 17
Showing the 200 most cited of 212.