Theorems · Inductive type · nonassociative algebras
LieAlgebra.IsSolvable
(L : Type v) → [LieRing L] → Prop
A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).
- Defined in
- Mathlib.Algebra.Lie.Solvable
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- LieRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LieRingstatement · cited by 1,548
Cited by27
Results whose statement or proof uses this declaration.
- LieAlgebra.radicalproof · cited by 13
- LieAlgebra.isSolvable_iffstatement · cited by 5
- LieAlgebra.IsSolvable.solvablestatement and proof · cited by 3
- LieAlgebra.center_le_radicalproof · cited by 2
- LieIdeal.isSolvable_of_killingForm_apply_lie_eq_zerostatement · cited by 2
- Function.Injective.lieAlgebra_isSolvablestatement and proof · cited by 2
- LieAlgebra.LieIdeal.solvable_iff_le_radicalstatement and proof · cited by 2
- LieModule.exists_nontrivial_weightSpace_of_isSolvablestatement and proof · cited by 1
- LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvablestatement and proof · cited by 1
- LieAlgebra.solvable_iff_equiv_solvablestatement and proof · cited by 1
- LieAlgebra.IsSolvable.casesOnstatement and proof · cited by 1
- LieAlgebra.IsSolvable.mkstatement · cited by 1