Theorems · Inductive type · nonassociative algebras
LieModule.IsNilpotent
(L : Type v) → (M : Type w) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → [LieRingModule L M] → Prop
A Lie module is nilpotent if its lower central series reaches 0 (in a finite number of steps).
- Defined in
- Mathlib.Algebra.Lie.Nilpotent
- Cited by
- 46 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement · cited by 12,871
- LieRingstatement · cited by 1,548
- LieRingModulestatement · cited by 727
Cited by51
Results whose statement or proof uses this declaration.
- LieRing.IsNilpotentproof · cited by 176
- LieModule.isNilpotent_iffstatement · cited by 13
- LieModule.IsNilpotent.nilpotentstatement and proof · cited by 8
- LieAlgebra.IsEngelianproof · cited by 5
- LieModule.isNilpotent_iff_forall'statement · cited by 3
- LieSubmodule.isNilpotent_iff_exists_self_le_ucsstatement · cited by 3
- LieModule.exists_forall_pow_toEnd_eq_zerostatement and proof · cited by 3
- LieModule.isNilpotent_iff_forallstatement and proof · cited by 2
- LieModule.isNilpotent_range_toEnd_iffstatement · cited by 2
- Function.Surjective.lieModuleIsNilpotentstatement and proof · cited by 2
- LieModule.maxNilpotentSubmoduleproof · cited by 2
- LieModule.nontrivial_lowerCentralSeriesLaststatement and proof · cited by 2