Structures · Algebra
LieAlgebra.IsSolvable
A Lie algebra is solvable if its derived series reaches 0 (in a finite number of steps).
- Defined in
- Mathlib.Algebra.Lie.Solvable
- Shape
- One type argument · adds solvable_int
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances2
- TensorProduct
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by15
- LieAlgebra.IsSolvable.solvable
- Function.Injective.lieAlgebra_isSolvable
- LieModule.exists_nontrivial_weightSpace_of_isSolvable
- LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable
- LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff
- LieAlgebra.radical_eq_top_of_isSolvable
- LieAlgebra.derivedSeries_lt_top_of_solvable
- Function.Surjective.lieAlgebra_isSolvable
- LieAlgebra.instIsSolvableTensorProduct
- LieAlgebra.instIsSolvableSubtypeMemLieSubalgebraTop
- LieAlgebra.isSolvableAdd
- LieAlgebra.derivedLength_zero
- LieAlgebra.IsSolvable.solvable_int
- LieHom.isSolvable_range
- Function.instIsSolvableSubtypeMemLieIdeal
Ancestors0
No ancestors.