Solvable

📁 Source: Mathlib/GroupTheory/Solvable.lean

Statistics

Metric	Count
Definitions `IsSolvable`, `derivedSeries`	2
Theorems `isSolvable`, `fin_5_not_solvable`, `not_solvable`, `comm_iff_isSolvable`, `derivedSeries_succ`, `commutator_lt_of_ne_bot`, `commutator_lt_top_of_nontrivial`, `solvable`, `derivedSeries_antitone`, `derivedSeries_characteristic`, `derivedSeries_le_map_derivedSeries`, `derivedSeries_normal`, `derivedSeries_one`, `derivedSeries_succ`, `derivedSeries_zero`, `isSolvable_def`, `isSolvable_iff_commutator_lt`, `isSolvable_of_comm`, `isSolvable_of_subsingleton`, `isSolvable_of_top_eq_bot`, `map_derivedSeries_eq`, `map_derivedSeries_le_derivedSeries`, `not_solvable_of_mem_derivedSeries`, `solvable_of_ker_le_range`, `solvable_of_solvable_injective`, `solvable_of_surjective`, `solvable_prod`, `solvable_quotient_of_solvable`, `subgroup_solvable_of_solvable`	29
Total	31

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSolvable` 📖	mathematical	—	`IsSolvable` `toGroup`	—	`le_bot_iff` `Abelianization.commutator_subset_ker`

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fin_5_not_solvable` 📖	mathematical	—	`IsSolvable` `Equiv.Perm` `permGroup`	—	`not_solvable_of_mem_derivedSeries` `Subgroup.mem_top` `Subgroup.Normal.mem_comm_iff` `derivedSeries_normal` `inv_mul_cancel_left` `Subgroup.commutator_mem_commutator` `Subgroup.Normal.conj_mem`
`not_solvable` 📖	mathematical	—	`IsSolvable` `Equiv.Perm` `permGroup`	—	`Nat.instAtLeastTwoHAddOfNat` `Cardinal.lift_mk_le` `Cardinal.mk_fin` `Cardinal.lift_natCast` `Cardinal.lift_id` `fin_5_not_solvable` `solvable_of_solvable_injective` `viaEmbeddingHom_injective`

IsSimpleGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm_iff_isSolvable` 📖	mathematical	—	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `IsSolvable`	—	`isSolvable_of_comm` `Subgroup.mem_bot` `Subgroup.mem_top` `mul_inv_eq_one` `mul_inv_rev` `mul_assoc` `derivedSeries_succ` `commutator_eq_closure` `Subgroup.subset_closure`
`derivedSeries_succ` 📖	mathematical	—	`derivedSeries` `commutator`	—	`derivedSeries_one` `derivedSeries_succ` `commutator.eq_1` `Subgroup.Normal.eq_bot_or_eq_top` `Subgroup.commutator_normal` `Subgroup.normal_top` `Subgroup.commutator_bot_left`

IsSolvable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_lt_of_ne_bot` 📖	mathematical	—	`Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Bracket.bracket` `Subgroup.commutator`	—	`Subgroup.range_subtype` `MonoidHom.range_eq_map` `Subgroup.map_commutator` `Subgroup.map_subtype_lt_map_subtype` `commutator_lt_top_of_nontrivial` `subgroup_solvable_of_solvable` `Subgroup.nontrivial_iff_ne_bot`
`commutator_lt_top_of_nontrivial` 📖	mathematical	—	`Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator` `Top.top` `Subgroup.instTop`	—	`lt_top_iff_ne_top` `Mathlib.Tactic.Contrapose.contrapose₃` `ne_of_eq_of_ne` `derivedSeries_zero` `derivedSeries_succ` `top_ne_bot` `Subgroup.instNontrivial`
`solvable` 📖	mathematical	—	`derivedSeries` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	—

(root)

Definitions

Name	Category	Theorems
`IsSolvable` 📖	CompData	33 math math: `isSolvable_of_comm`, `solvable_of_ker_le_range`, `IsNilpotent.to_isSolvable`, `subgroup_solvable_of_solvable`, `solvable_of_surjective`, `gal_X_pow_isSolvable`, `solvable_prod`, `solvableByRad.isSolvable'`, `IsSimpleGroup.comm_iff_isSolvable`, `gal_X_pow_sub_C_isSolvable`, `not_solvable_of_mem_derivedSeries`, `solvableByRad.isSolvable`, `gal_X_pow_sub_C_isSolvable_aux`, `gal_X_pow_sub_one_isSolvable`, `isSolvable_of_subsingleton`, `CommGroup.isSolvable`, `Equiv.Perm.not_solvable`, `isSolvable_of_top_eq_bot`, `solvable_of_solvable_injective`, `gal_C_isSolvable`, `isSolvable_of_isScalarTower`, `IsZGroup.instIsSolvableOfFinite`, `gal_X_sub_C_isSolvable`, `isSolvable_def`, `gal_one_isSolvable`, `Equiv.Perm.fin_5_not_solvable`, `solvable_quotient_of_solvable`, `gal_mul_isSolvable`, `isSolvable_iff_commutator_lt`, `gal_zero_isSolvable`, `gal_isSolvable_of_splits`, `gal_X_isSolvable`, `gal_isSolvable_tower`
`derivedSeries` 📖	CompOp	13 math math: `derivedSeries_le_map_derivedSeries`, `derivedSeries_zero`, `map_derivedSeries_eq`, `derivedSeries_succ`, `derivedSeries_antitone`, `map_derivedSeries_le_derivedSeries`, `IsSimpleGroup.derivedSeries_succ`, `derivedSeries_characteristic`, `isSolvable_def`, `derivedSeries_one`, `derived_le_lower_central`, `derivedSeries_normal`, `IsSolvable.solvable`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivedSeries_antitone` 📖	mathematical	—	`Antitone` `Subgroup` `Nat.instPreorder` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `derivedSeries`	—	`antitone_nat_of_succ_le` `Subgroup.commutator_le_self`
`derivedSeries_characteristic` 📖	mathematical	—	`Subgroup.Characteristic` `derivedSeries`	—	`Subgroup.topCharacteristic` `Subgroup.commutator_characteristic`
`derivedSeries_le_map_derivedSeries` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `derivedSeries` `Subgroup.map`	—	`Eq.ge` `Subgroup.map_top_of_surjective` `Subgroup.commutator_le_map_commutator`
`derivedSeries_normal` 📖	mathematical	—	`Subgroup.Normal` `derivedSeries`	—	`Subgroup.normal_of_characteristic` `Subgroup.topCharacteristic` `Subgroup.commutator_normal`
`derivedSeries_one` 📖	mathematical	—	`derivedSeries` `commutator`	—	—
`derivedSeries_succ` 📖	mathematical	—	`derivedSeries` `Bracket.bracket` `Subgroup` `Subgroup.commutator`	—	—
`derivedSeries_zero` 📖	mathematical	—	`derivedSeries` `Top.top` `Subgroup` `Subgroup.instTop`	—	—
`isSolvable_def` 📖	mathematical	—	`IsSolvable` `derivedSeries` `Bot.bot` `Subgroup` `Subgroup.instBot`	—	—
`isSolvable_iff_commutator_lt` 📖	mathematical	—	`IsSolvable` `Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Bracket.bracket` `Subgroup.commutator`	—	`IsSolvable.commutator_lt_of_ne_bot` `WellFoundedLT.induction` `eq_or_ne` `isSolvable_of_subsingleton` `Unique.instSubsingleton` `Subgroup.map_injective` `Subgroup.subtype_injective` `Subgroup.map_bot` `derivedSeries_succ` `derivedSeries_zero` `Subgroup.map_commutator` `MonoidHom.range_eq_map` `Subgroup.range_subtype` `solvable_of_surjective` `MonoidHom.range_eq_top`
`isSolvable_of_comm` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`IsSolvable`	—	`CommGroup.isSolvable`
`isSolvable_of_subsingleton` 📖	mathematical	—	`IsSolvable`	—	`isSolvable_of_top_eq_bot` `Unique.instSubsingleton`
`isSolvable_of_top_eq_bot` 📖	mathematical	`Top.top` `Subgroup` `Subgroup.instTop` `Bot.bot` `Subgroup.instBot`	`IsSolvable`	—	—
`map_derivedSeries_eq` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Subgroup.map` `derivedSeries`	—	`le_antisymm` `map_derivedSeries_le_derivedSeries` `derivedSeries_le_map_derivedSeries`
`map_derivedSeries_le_derivedSeries` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.map` `derivedSeries`	—	`le_top` `Subgroup.map_commutator`
`not_solvable_of_mem_derivedSeries` 📖	mathematical	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `derivedSeries`	`IsSolvable`	—	`isSolvable_def` `Subgroup.mem_bot`
`solvable_of_ker_le_range` 📖	mathematical	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.range`	`IsSolvable`	—	`le_bot_iff` `LE.le.trans` `Subgroup.map_eq_bot_iff` `map_derivedSeries_le_derivedSeries` `Eq.le` `MonoidHom.range_eq_map` `Subgroup.commutator_le_map_commutator` `Subgroup.map_bot`
`solvable_of_solvable_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsSolvable`	—	`solvable_of_ker_le_range` `bot_le` `MonoidHom.ker_eq_bot_iff`
`solvable_of_surjective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsSolvable`	—	`solvable_of_ker_le_range` `le_top` `MonoidHom.range_eq_top_of_surjective`
`solvable_prod` 📖	mathematical	—	`IsSolvable` `Prod.instGroup`	—	`solvable_of_ker_le_range`
`solvable_quotient_of_solvable` 📖	mathematical	—	`IsSolvable` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `QuotientGroup.Quotient.group`	—	`solvable_of_surjective` `QuotientGroup.mk'_surjective`
`subgroup_solvable_of_solvable` 📖	mathematical	—	`IsSolvable` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	—	`solvable_of_solvable_injective` `Subgroup.subtype_injective`

---

← Back to Index