Solvable

📁 Source: Mathlib/Algebra/Lie/Solvable.lean

Statistics

Metric	Count
Definitions `IsSolvable`, `derivedAbelianOfIdeal`, `derivedLength`, `derivedLengthOfIdeal`, `derivedSeries`, `derivedSeriesOfIdeal`, `instUniqueSubtypeMemLieIdealBot`, `radical`	8
Theorems `lieAlgebra_isSolvable`, `lieAlgebra_isSolvable`, `instIsSolvableSubtypeMemLieSubmodule`, `mk`, `solvable`, `solvable_int`, `solvable_iff_le_radical`, `abelian_derivedAbelianOfIdeal`, `abelian_iff_derived_one_eq_bot`, `abelian_iff_derived_succ_eq_bot`, `abelian_of_solvable_ideal_eq_bot_iff`, `center_le_radical`, `derivedLength_eq_derivedLengthOfIdeal`, `derivedLength_zero`, `derivedSeriesOfIdeal_add`, `derivedSeriesOfIdeal_add_le_add`, `derivedSeriesOfIdeal_antitone`, `derivedSeriesOfIdeal_baseChange`, `derivedSeriesOfIdeal_le`, `derivedSeriesOfIdeal_le_self`, `derivedSeriesOfIdeal_mono`, `derivedSeriesOfIdeal_succ`, `derivedSeriesOfIdeal_succ_le`, `derivedSeriesOfIdeal_zero`, `derivedSeries_baseChange`, `derivedSeries_def`, `derivedSeries_lt_top_of_solvable`, `derivedSeries_of_bot_eq_bot`, `derivedSeries_of_derivedLength_succ`, `instIsSolvableSubtypeMemLieSubalgebraTop`, `instIsSolvableTensorProduct`, `isSolvableAdd`, `isSolvableBot`, `isSolvable_iff`, `isSolvable_iff_int`, `isSolvable_tensorProduct_iff`, `le_solvable_ideal_solvable`, `ofAbelianIsSolvable`, `radicalIsSolvable`, `radical_eq_top_of_isSolvable`, `solvable_iff_equiv_solvable`, `isSolvable_range`, `coe_derivedSeries_eq_int`, `derivedSeries_add_eq_bot`, `derivedSeries_eq_bot_iff`, `derivedSeries_eq_derivedSeriesOfIdeal_comap`, `derivedSeries_eq_derivedSeriesOfIdeal_map`, `derivedSeries_eq_top`, `derivedSeries_map_eq`, `derivedSeries_map_le`, `derivedSeries_succ_eq_top_iff`	51
Total	59

Function

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsSolvableSubtypeMemLieSubmodule` 📖	mathematical	—	`LieAlgebra.IsSolvable` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lieRing`	—	`Injective.lieAlgebra_isSolvable` `LieIdeal.incl_injective`

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lieAlgebra_isSolvable` 📖	mathematical	`DFunLike.coe` `LieHom` `LieHom.instFunLike`	`LieAlgebra.IsSolvable`	—	`LieAlgebra.isSolvable_iff` `LieIdeal.bot_of_map_eq_bot` `eq_bot_iff` `LieIdeal.derivedSeries_map_le`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lieAlgebra_isSolvable` 📖	mathematical	`DFunLike.coe` `LieHom` `LieHom.instFunLike`	`LieAlgebra.IsSolvable`	—	`LieAlgebra.isSolvable_iff` `LieIdeal.derivedSeries_map_eq`

LieAlgebra

Definitions

Name	Category	Theorems
`IsSolvable` 📖	CompData	18 math math: `isSolvable_iff_int`, `ofAbelianIsSolvable`, `le_solvable_ideal_solvable`, `IsSolvable.mk`, `instIsSolvableSubtypeMemLieSubalgebraTop`, `isSolvable_iff`, `instIsSolvableTensorProduct`, `Function.Injective.lieAlgebra_isSolvable`, `isSolvable_of_isNilpotent`, `LieHom.isSolvable_range`, `radicalIsSolvable`, `solvable_iff_equiv_solvable`, `Function.Surjective.lieAlgebra_isSolvable`, `isSolvableAdd`, `isSolvable_tensorProduct_iff`, `isSolvableBot`, `LieIdeal.solvable_iff_le_radical`, `Function.instIsSolvableSubtypeMemLieSubmodule`
`derivedAbelianOfIdeal` 📖	CompOp	2 math math: `abelian_of_solvable_ideal_eq_bot_iff`, `abelian_derivedAbelianOfIdeal`
`derivedLength` 📖	CompOp	1 math math: `derivedLength_eq_derivedLengthOfIdeal`
`derivedLengthOfIdeal` 📖	CompOp	3 math math: `derivedLength_zero`, `derivedSeries_of_derivedLength_succ`, `derivedLength_eq_derivedLengthOfIdeal`
`derivedSeries` 📖	CompOp	15 math math: `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map`, `LieIdeal.derivedSeries_map_eq`, `isSolvable_iff_int`, `LieModule.derivedSeries_le_lowerCentralSeries`, `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap`, `LieIdeal.derivedSeries_map_le`, `isSolvable_iff`, `IsSolvable.solvable_int`, `derivedSeries_baseChange`, `derivedSeries_def`, `LieIdeal.derivedSeries_eq_bot_iff`, `LieIdeal.coe_derivedSeries_eq_int`, `derivedSeries_lt_top_of_solvable`, `LieIdeal.derivedSeries_succ_eq_top_iff`, `IsSolvable.solvable`
`derivedSeriesOfIdeal` 📖	CompOp	18 math math: `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map`, `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap`, `derivedSeriesOfIdeal_succ_le`, `derivedSeries_of_derivedLength_succ`, `derivedSeriesOfIdeal_le_self`, `derivedSeriesOfIdeal_succ`, `abelian_iff_derived_one_eq_bot`, `derivedSeriesOfIdeal_antitone`, `derivedSeriesOfIdeal_add_le_add`, `derivedSeries_def`, `derivedSeriesOfIdeal_mono`, `derivedSeriesOfIdeal_le`, `LieIdeal.derivedSeries_eq_bot_iff`, `derivedSeriesOfIdeal_add`, `derivedSeries_of_bot_eq_bot`, `abelian_iff_derived_succ_eq_bot`, `derivedSeriesOfIdeal_baseChange`, `derivedSeriesOfIdeal_zero`
`instUniqueSubtypeMemLieIdealBot` 📖	CompOp	—
`radical` 📖	CompOp	11 math math: `abelian_radical_of_hasTrivialRadical`, `hasCentralRadical_iff`, `hasTrivialRadical_iff`, `abelian_radical_iff_solvable_is_abelian`, `radical_eq_top_of_isSolvable`, `HasCentralRadical.radical_eq_center`, `center_le_radical`, `HasTrivialRadical.radical_eq_bot`, `radicalIsSolvable`, `maxNilpotentIdeal_le_radical`, `LieIdeal.solvable_iff_le_radical`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abelian_derivedAbelianOfIdeal` 📖	mathematical	—	`IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `derivedAbelianOfIdeal` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `LieIdeal.isLieAbelian_of_trivial` `LieModule.instIsTrivialOfSubsingleton'` `Unique.instSubsingleton` `derivedSeries_of_derivedLength_succ`
`abelian_iff_derived_one_eq_bot` 📖	mathematical	—	`IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `derivedSeriesOfIdeal` `Bot.bot` `LieIdeal` `LieSubmodule.instBot`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `derivedSeriesOfIdeal_succ` `derivedSeriesOfIdeal_zero` `LieSubmodule.lie_abelian_iff_lie_self_eq_bot`
`abelian_iff_derived_succ_eq_bot` 📖	mathematical	—	`IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `derivedSeriesOfIdeal` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `Bot.bot` `LieIdeal` `LieSubmodule.instBot`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `add_comm` `derivedSeriesOfIdeal_add` `abelian_iff_derived_one_eq_bot`
`abelian_of_solvable_ideal_eq_bot_iff` 📖	mathematical	—	`derivedAbelianOfIdeal` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `derivedSeries_of_derivedLength_succ` `derivedSeries_of_bot_eq_bot`
`center_le_radical` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `center` `radical`	—	`ofAbelianIsSolvable` `instIsLieAbelianSubtypeMemLieSubmoduleCenter` `le_sSup`
`derivedLength_eq_derivedLengthOfIdeal` 📖	mathematical	—	`derivedLength` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lieRing` `LieIdeal.lieAlgebra` `derivedLengthOfIdeal`	—	`Set.ext` `LieIdeal.derivedSeries_eq_bot_iff`
`derivedLength_zero` 📖	mathematical	—	`derivedLengthOfIdeal` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`IsSolvable.solvable` `LieIdeal.derivedSeries_eq_bot_iff` `derivedSeries_def` `Set.Nonempty.ne_empty`
`derivedSeriesOfIdeal_add` 📖	mathematical	—	`derivedSeriesOfIdeal`	—	`derivedSeriesOfIdeal_zero` `derivedSeriesOfIdeal_succ`
`derivedSeriesOfIdeal_add_le_add` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeriesOfIdeal` `LieSubmodule.instAdd`	—	`LieSubmodule.mono_lie` `LieSubmodule.lie_sup` `LieSubmodule.sup_lie` `OrderHom.iterate_sup_le_sup_iff`
`derivedSeriesOfIdeal_antitone` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeriesOfIdeal`	—	`derivedSeriesOfIdeal_le` `le_refl`
`derivedSeriesOfIdeal_baseChange` 📖	mathematical	—	`derivedSeriesOfIdeal` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `ExtendScalars.instLieRing` `ExtendScalars.instLieAlgebra` `LieSubmodule.baseChange` `lieRingSelfModule` `lieAlgebraSelfModule`	—	`lieAlgebraSelfModule` `Algebra.to_smulCommClass` `derivedSeriesOfIdeal_succ` `LieSubmodule.lie_baseChange`
`derivedSeriesOfIdeal_le` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	`derivedSeriesOfIdeal`	—	`le_zero_iff` `derivedSeriesOfIdeal_zero` `le_iff_eq_or_lt` `derivedSeriesOfIdeal_succ` `LieSubmodule.mono_lie` `le_refl` `le_trans` `LieSubmodule.lie_le_left`
`derivedSeriesOfIdeal_le_self` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeriesOfIdeal`	—	`derivedSeriesOfIdeal_le` `le_refl` `zero_le` `Nat.instCanonicallyOrderedAdd`
`derivedSeriesOfIdeal_mono` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	`derivedSeriesOfIdeal`	—	`derivedSeriesOfIdeal_le` `le_refl`
`derivedSeriesOfIdeal_succ` 📖	mathematical	—	`derivedSeriesOfIdeal` `Bracket.bracket` `LieIdeal` `LieSubmodule.hasBracket` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`Function.iterate_succ_apply'`
`derivedSeriesOfIdeal_succ_le` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeriesOfIdeal`	—	`derivedSeriesOfIdeal_le` `le_refl`
`derivedSeriesOfIdeal_zero` 📖	mathematical	—	`derivedSeriesOfIdeal`	—	—
`derivedSeries_baseChange` 📖	mathematical	—	`derivedSeries` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `ExtendScalars.instLieRing` `ExtendScalars.instLieAlgebra` `LieSubmodule.baseChange` `lieRingSelfModule` `lieAlgebraSelfModule`	—	`lieAlgebraSelfModule` `derivedSeries_def` `derivedSeriesOfIdeal_baseChange` `Algebra.to_smulCommClass` `LieSubmodule.baseChange_top`
`derivedSeries_def` 📖	mathematical	—	`derivedSeries` `derivedSeriesOfIdeal` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	—
`derivedSeries_lt_top_of_solvable` 📖	mathematical	—	`LieIdeal` `Preorder.toLT` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeries` `Top.top` `LieSubmodule.instTop`	—	`IsSolvable.solvable` `lt_top_iff_ne_top` `top_ne_bot` `LieSubmodule.instNontrivial` `LieIdeal.derivedSeries_eq_top`
`derivedSeries_of_bot_eq_bot` 📖	mathematical	—	`derivedSeriesOfIdeal` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`eq_bot_iff` `derivedSeriesOfIdeal_le_self`
`derivedSeries_of_derivedLength_succ` 📖	mathematical	—	`derivedLengthOfIdeal` `IsLieAbelian` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `derivedSeriesOfIdeal` `LieRingModule.toBracket` `LieIdeal.lieRing` `LieIdeal.lieRingModule` `LieSubmodule.instLieRingModuleSubtypeMem` `ZeroMemClass.zero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `abelian_iff_derived_succ_eq_bot` `derivedSeriesOfIdeal_antitone` `eq_bot_iff` `Nat.sInf_upward_closed_eq_succ_iff`
`instIsSolvableSubtypeMemLieSubalgebraTop` 📖	mathematical	—	`IsSolvable` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `Top.top` `LieSubalgebra.instTop` `LieSubalgebra.lieRing`	—	`solvable_iff_equiv_solvable`
`instIsSolvableTensorProduct` 📖	mathematical	—	`IsSolvable` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `ExtendScalars.instLieRing`	—	`IsSolvable.solvable` `isSolvable_iff` `lieAlgebraSelfModule` `derivedSeries_baseChange` `Algebra.to_smulCommClass` `LieSubmodule.baseChange_bot`
`isSolvableAdd` 📖	mathematical	—	`IsSolvable` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal` `LieSubmodule.instAdd` `LieIdeal.lieRing`	—	`IsSolvable.solvable` `LieIdeal.derivedSeries_add_eq_bot`
`isSolvableBot` 📖	mathematical	—	`IsSolvable` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieIdeal.lieRing`	—	`LieIdeal.subsingleton_of_bot`
`isSolvable_iff` 📖	mathematical	—	`IsSolvable` `derivedSeries` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`LieIdeal.coe_derivedSeries_eq_int`
`isSolvable_iff_int` 📖	mathematical	—	`IsSolvable` `derivedSeries` `Int.instCommRing` `LieRing.instLieAlgebra` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	—
`isSolvable_tensorProduct_iff` 📖	mathematical	—	`IsSolvable` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `ExtendScalars.instLieRing`	—	`isSolvable_iff` `eq_bot_iff` `LieSubmodule.mem_bot` `Module.FaithfullyFlat.one_tmul_eq_zero_iff` `lieAlgebraSelfModule` `derivedSeries_baseChange` `Submodule.tmul_mem_baseChange_of_mem` `instIsSolvableTensorProduct`
`le_solvable_ideal_solvable` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	`IsSolvable` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lieRing`	—	`Function.Injective.lieAlgebra_isSolvable` `LieIdeal.inclusion_injective`
`ofAbelianIsSolvable` 📖	mathematical	—	`IsSolvable`	—	`AddSubmonoidClass.toZeroMemClass` `AddSubgroupClass.toAddSubmonoidClass` `LieSubmodule.instAddSubgroupClass` `abelian_iff_derived_one_eq_bot` `lie_abelian_iff_equiv_lie_abelian`
`radicalIsSolvable` 📖	mathematical	—	`IsSolvable` `LieSubmodule` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `radical` `LieIdeal.lieRing`	—	`LieSubmodule.wellFoundedGT_of_noetherian` `CompleteLattice.isSupClosedCompact_iff_wellFoundedGT` `isSolvableBot` `Set.mem_setOf_eq` `isSolvableAdd`
`radical_eq_top_of_isSolvable` 📖	mathematical	—	`radical` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule`	—	`eq_top_iff` `instIsSolvableSubtypeMemLieSubalgebraTop` `le_sSup`
`solvable_iff_equiv_solvable` 📖	mathematical	—	`IsSolvable`	—	`Function.Injective.lieAlgebra_isSolvable` `LieEquiv.injective`

LieAlgebra.IsSolvable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk` 📖	mathematical	`LieAlgebra.derivedSeries` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	`LieAlgebra.IsSolvable`	—	`LieAlgebra.isSolvable_iff`
`solvable` 📖	mathematical	—	`LieAlgebra.derivedSeries` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`LieAlgebra.isSolvable_iff`
`solvable_int` 📖	mathematical	—	`LieAlgebra.derivedSeries` `Int.instCommRing` `LieRing.instLieAlgebra` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	—

LieAlgebra.LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`solvable_iff_le_radical` 📖	mathematical	—	`LieAlgebra.IsSolvable` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieIdeal.lieRing` `LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieAlgebra.radical`	—	`le_sSup` `LieAlgebra.le_solvable_ideal_solvable` `LieAlgebra.radicalIsSolvable`

LieHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSolvable_range` 📖	mathematical	—	`LieAlgebra.IsSolvable` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `range` `LieSubalgebra.lieRing`	—	`Function.Surjective.lieAlgebra_isSolvable` `surjective_rangeRestrict`

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_derivedSeries_eq_int` 📖	mathematical	—	`SetLike.coe` `LieIdeal` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieAlgebra.derivedSeries` `Int.instCommRing` `LieRing.instLieAlgebra`	—	`LieSubmodule.coe_toSubmodule` `LieAlgebra.derivedSeries_def` `LieAlgebra.derivedSeriesOfIdeal_succ` `LieSubmodule.lieIdeal_oper_eq_linear_span'` `lieAlgebraSelfModule` `instLieModuleInt` `Set.ext_iff` `le_antisymm` `AddCommGroup.intIsScalarTower`
`derivedSeries_add_eq_bot` 📖	mathematical	`LieAlgebra.derivedSeries` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `Bot.bot` `LieIdeal` `LieSubmodule.instBot`	`LieSubmodule.instAdd`	—	`derivedSeries_eq_bot_iff` `le_bot_iff` `LieAlgebra.derivedSeriesOfIdeal_add_le_add` `sup_of_le_left`
`derivedSeries_eq_bot_iff` 📖	mathematical	—	`LieAlgebra.derivedSeries` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `Bot.bot` `LieIdeal` `LieSubmodule.instBot` `LieAlgebra.derivedSeriesOfIdeal`	—	`derivedSeries_eq_derivedSeriesOfIdeal_map` `map_eq_bot_iff` `ker_incl` `eq_bot_iff`
`derivedSeries_eq_derivedSeriesOfIdeal_comap` 📖	mathematical	—	`LieAlgebra.derivedSeries` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `comap` `incl` `LieAlgebra.derivedSeriesOfIdeal`	—	`comap_incl_self` `LieAlgebra.derivedSeriesOfIdeal_succ` `comap_bracket_incl_of_le` `LieAlgebra.derivedSeriesOfIdeal_le_self`
`derivedSeries_eq_derivedSeriesOfIdeal_map` 📖	mathematical	—	`map` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `incl` `LieAlgebra.derivedSeries` `LieAlgebra.derivedSeriesOfIdeal`	—	`derivedSeries_eq_derivedSeriesOfIdeal_comap` `map_comap_incl` `inf_eq_right` `LieAlgebra.derivedSeriesOfIdeal_le_self`
`derivedSeries_eq_top` 📖	—	`LieAlgebra.derivedSeries` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	—	`derivedSeries_succ_eq_top_iff`
`derivedSeries_map_eq` 📖	mathematical	`DFunLike.coe` `LieHom` `LieHom.instFunLike`	`map` `LieAlgebra.derivedSeries`	—	`LieHom.idealRange_eq_map` `LieHom.idealRange_eq_top_of_surjective` `LieAlgebra.derivedSeriesOfIdeal_succ` `map_bracket_eq`
`derivedSeries_map_le` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `map` `LieAlgebra.derivedSeries`	—	`LieAlgebra.derivedSeriesOfIdeal_succ` `le_trans` `map_bracket_le` `LieSubmodule.mono_lie`
`derivedSeries_succ_eq_top_iff` 📖	mathematical	—	`LieAlgebra.derivedSeries` `Top.top` `LieIdeal` `LieSubmodule.instTop` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`zero_add` `LieAlgebra.derivedSeriesOfIdeal_succ` `eq_top_iff` `LieSubmodule.lie_le_right`

---

← Back to Index