Theorems · Definition · nonassociative algebras
LieSubalgebra.engel
(R : Type u_1) →
{L : Type u_2} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → L → LieSubalgebra R LThe Engel subalgebra Engel R x consists of
all y : L such that (ad R L x)^n kills y for some n.
Engel subalgebras are self-normalizing (LieSubalgebra.normalizer_engel),
and minimal ones are nilpotent, hence Cartan subalgebras.
- Defined in
- Mathlib.Algebra.Lie.EngelSubalgebra
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingLieRingLieAlgebra
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- CommRingstatement and proof · cited by 17,173
- Submoduleproof · cited by 7,192
- LieRingstatement and proof · cited by 1,548
- LieAlgebrastatement and proof · cited by 1,246
- LieSubalgebrastatement · cited by 418
- LieAlgebra.adproof · cited by 49
- Module.End.maxGenEigenspaceproof · cited by 41
Cited by13
Results whose statement or proof uses this declaration.
- LieSubalgebra.self_mem_engelstatement · cited by 4
- LieSubalgebra.mem_engel_iffstatement · cited by 4
- LieAlgebra.finrank_engelstatement · cited by 2
- LieSubalgebra.isNilpotent_of_forall_le_engelstatement and proof · cited by 1
- LieAlgebra.isRegular_iff_finrank_engel_eq_rankstatement and proof · cited by 1
- LieSubalgebra.engel_zerostatement · cited by 1
- LieAlgebra.rank_le_finrank_engelstatement · cited by 1
- LieAlgebra.engel_isBot_of_isMinstatement and proof · cited by 1
- LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_cardstatement and proof · cited by 1
- LieSubalgebra.normalizer_engelstatement and proof · cited by 1
- LieSubalgebra.engel_carrierstatement · cited by 0
- LieAlgebra.exists_isCartanSubalgebra_engelstatement · cited by 0