Documentation Verification Report

AbelRuffini

📁 Source: Mathlib/FieldTheory/AbelRuffini.lean

Statistics

Metric	Count
Definitions `IsSolvableByRad`, `solvableByRad`, `P`	3
Theorems `gal_C_isSolvable`, `gal_X_isSolvable`, `gal_X_pow_isSolvable`, `gal_X_pow_sub_C_isSolvable`, `gal_X_pow_sub_C_isSolvable_aux`, `gal_X_pow_sub_one_isSolvable`, `gal_X_sub_C_isSolvable`, `gal_isSolvable_of_splits`, `gal_isSolvable_tower`, `gal_mul_isSolvable`, `gal_one_isSolvable`, `gal_prod_isSolvable`, `gal_zero_isSolvable`, `induction`, `induction1`, `induction2`, `induction3`, `isIntegral`, `isSolvable`, `isSolvable'`, `splits_X_pow_sub_one_of_X_pow_sub_C`	21
Total	24

(root)

Definitions

Name	Category	Theorems
`IsSolvableByRad` 📖	CompData	—
`solvableByRad` 📖	CompOp	2 math math: `solvableByRad.isSolvable`, `solvableByRad.isIntegral`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`gal_C_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`gal_X_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial.X` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`gal_X_pow_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`gal_X_pow_sub_C_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instGroupGal`	—	`Polynomial.C_0` `sub_zero` `gal_X_pow_isSolvable` `gal_isSolvable_tower` `splits_X_pow_sub_one_of_X_pow_sub_C` `Polynomial.SplittingField.splits` `gal_X_pow_sub_one_isSolvable` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.map_C` `gal_X_pow_sub_C_isSolvable_aux` `Polynomial.map_id` `Polynomial.map_one`
`gal_X_pow_sub_C_isSolvable_aux` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instOne`	`IsSolvable` `Polynomial.Gal` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instGroupGal`	—	`Polynomial.C_0` `sub_zero` `gal_X_pow_isSolvable` `injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `pow_zero` `Polynomial.C_1` `Polynomial.C_sub` `gal_C_isSolvable` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Polynomial.X_pow_sub_C_ne_zero` `RingHom.mem_range` `minpoly.mem_range_of_degree_eq_one` `Polynomial.Splits.degree_eq_one_of_irreducible` `Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.map_ne_zero` `minpoly.dvd` `Polynomial.map_id` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `sub_eq_zero` `Polynomial.aeval_X_pow` `Polynomial.aeval_one` `minpoly.irreducible` `Normal.isIntegral` `Polynomial.SplittingField.instNormal` `isSolvable_of_comm` `Polynomial.Gal.ext` `zero_pow` `Polynomial.aeval_C` `Polynomial.mem_rootSet_of_ne` `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField` `div_pow` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgEquivClass.toAlgHomClass` `AlgEquiv.commutes` `div_self` `mul_div_cancel₀` `AlgEquiv.mul_apply` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgEquiv.instAlgEquivClass` `mul_assoc` `mul_right_inj'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `mul_comm`
`gal_X_pow_sub_one_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instOne` `Polynomial.instGroupGal`	—	`pow_zero` `sub_self` `gal_zero_isSolvable` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Polynomial.X_pow_sub_C_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isSolvable_of_comm` `Polynomial.Gal.ext` `instIsDomain` `CanLift.prf` `Nat.canLiftPNat` `map_rootsOfUnity_eq_pow_self` `NeZero.pnat` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.mem_rootSet_of_ne` `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `Polynomial.aeval_X_pow` `Polynomial.aeval_one` `AlgEquiv.mul_apply` `map_pow` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass` `pow_mul` `pow_mul'`
`gal_X_sub_C_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`gal_isSolvable_of_splits` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	—	`solvable_of_surjective` `Polynomial.Gal.instIsScalarTowerSplittingField` `Polynomial.SplittingField.instNormal` `AlgEquiv.restrictNormalHom_surjective`
`gal_isSolvable_tower` 📖	mathematical	`Polynomial.Splits` `Polynomial.SplittingField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.SplittingField.instField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	—	`Polynomial.IsSplittingField.map` `Polynomial.Gal.instIsScalarTowerSplittingField` `Polynomial.IsSplittingField.splittingField` `MulEquiv.injective` `isSolvable_of_isScalarTower` `Polynomial.SplittingField.instNormal` `solvable_of_solvable_injective`
`gal_mul_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instMul` `Polynomial.instGroupGal`	—	`solvable_of_solvable_injective` `Polynomial.Gal.restrictProd_injective` `solvable_prod`
`gal_one_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instOne` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`gal_prod_isSolvable` 📖	mathematical	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	`Multiset.prod` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommRing.toCommMonoid` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Multiset.induction_on'` `gal_one_isSolvable` `Multiset.insert_eq_cons` `Multiset.prod_cons` `gal_mul_isSolvable`
`gal_zero_isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instZero` `Polynomial.instGroupGal`	—	`isSolvable_of_subsingleton` `Unique.instSubsingleton`
`splits_X_pow_sub_one_of_X_pow_sub_C` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	`Polynomial.instOne`	—	`injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `pow_zero` `sub_self` `Polynomial.map_zero` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `ne_of_eq_of_ne` `Polynomial.degree_X_pow_sub_C` `WithBot.coe_eq_coe` `Polynomial.Splits.exists_eval_eq_zero` `Polynomial.degree_map` `zero_pow` `sub_eq_zero` `Polynomial.eval₂_C` `Polynomial.eval₂_X_pow` `Polynomial.eval₂_sub` `Polynomial.eval_map` `instIsDomain` `Polynomial.Splits.eq_prod_roots` `Polynomial.Splits.natDegree_eq_card_roots` `Polynomial.natDegree_map` `Polynomial.natDegree_X_pow_sub_C` `Polynomial.splits_iff_exists_multiset` `Polynomial.leadingCoeff_map` `Polynomial.leadingCoeff_X_pow_sub_one` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.C_1` `one_mul` `Multiset.map_map` `Polynomial.C_mul` `RingHom.map_mul` `inv_mul_cancel₀` `RingHom.map_one` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.map_C` `Polynomial.map_one` `Polynomial.sub_comp` `Polynomial.pow_comp` `Polynomial.X_comp` `Polynomial.C_comp` `mul_pow` `Polynomial.C_pow` `mul_sub` `mul_assoc` `mul_div_cancel₀` `Polynomial.leadingCoeff_X_pow_sub_C` `Polynomial.multiset_prod_comp` `Multiset.prod_map_mul` `Function.const_def` `Multiset.map_const` `Multiset.prod_replicate`

solvableByRad

Definitions

Name	Category	Theorems
`P` 📖	MathDef	3 math math: `induction2`, `induction3`, `induction1`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction` 📖	—	`DFunLike.coe` `RingHom` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `IntermediateField.toField` `RingHom.instFunLike` `algebraMap` `IntermediateField.algebra'` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `SubringClass.toNegMemClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Distrib.toMul` `InvMemClass.inv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `SubfieldClass.toInvMemClass`	—	—	`IsScalarTower.left` `SubringClass.toNegMemClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `SubfieldClass.toInvMemClass` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `IntermediateField.coe_pow` `Subtype.mem`
`induction1` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.adjoin` `Set` `Set.instSingletonSet`	`P`	—	`IsScalarTower.left` `induction2` `IntermediateField.adjoin.mono` `ge_of_eq` `Set.pair_eq_singleton`
`induction2` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `IntermediateField.toField` `IntermediateField.algebra'` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.toDistribMulAction` `Algebra.toModule` `IntermediateField.adjoin` `Set` `Set.instInsert` `Set.instSingletonSet`	`P`	—	`IsScalarTower.left` `Polynomial.SplittingField.splits` `IntermediateField.isScalarTower` `IntermediateField.nonempty_algHom_adjoin_of_splits` `isIntegral` `Polynomial.splits_mul_iff` `instIsDomain` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `minpoly.ne_zero` `Polynomial.map_mul` `minpoly.eq_of_irreducible_of_monic` `minpoly.irreducible` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `map_eq_zero` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `RingHom.injective` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `IntermediateField.isScalarTower_mid'` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHom.instRingHomClass` `minpoly.aeval` `minpoly.monic` `P.eq_1` `gal_isSolvable_of_splits` `Normal.splits` `Polynomial.SplittingField.instNormal` `gal_mul_isSolvable`
`induction3` 📖	mathematical	—	`P`	—	`SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsScalarTower.left` `Polynomial.comp_eq_zero_iff` `IsDomain.to_noZeroDivisors` `instIsDomain` `minpoly.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isIntegral` `Polynomial.natDegree_C` `Polynomial.natDegree_X_pow` `gal_isSolvable_of_splits` `Polynomial.Splits.of_dvd` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `Polynomial.map_dvd_map'` `minpoly.dvd` `Polynomial.aeval_comp` `Polynomial.aeval_X_pow` `minpoly.aeval` `gal_isSolvable_tower` `Polynomial.Gal.splits_in_splittingField_of_comp` `Polynomial.splits_iff_exists_multiset` `Polynomial.map_comp` `Polynomial.map_pow` `Polynomial.map_X` `Polynomial.mul_comp` `Polynomial.C_comp` `gal_mul_isSolvable` `gal_C_isSolvable` `Polynomial.multiset_prod_comp` `gal_prod_isSolvable` `Multiset.mem_map` `Polynomial.sub_comp` `Polynomial.X_comp` `gal_X_pow_sub_C_isSolvable`
`isIntegral` 📖	mathematical	—	`IsIntegral` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	`induction` `IsScalarTower.left` `isIntegral_algebraMap` `IsIntegral.add` `IsIntegral.neg` `IsIntegral.mul` `IsIntegral.inv` `SubsemiringClass.toSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsAlgebraic.isIntegral` `Polynomial.leadingCoeff_eq_zero` `mul_one` `one_pow` `Polynomial.leadingCoeff_X_pow` `Polynomial.leadingCoeff_comp` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natDegree_X_pow` `Polynomial.aeval_comp` `Polynomial.aeval_X_pow`
`isSolvable` 📖	mathematical	—	`IsSolvable` `Polynomial.Gal` `minpoly` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toField` `IntermediateField.algebra'` `CommRing.toCommSemiring` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `Polynomial.instGroupGal`	—	`induction` `IsScalarTower.left` `minpoly.eq_X_sub_C` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `gal_X_sub_C_isSolvable` `induction2` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `IntermediateField.subset_adjoin` `Set.mem_insert` `Set.mem_insert_of_mem` `Set.mem_singleton` `induction1` `SubringClass.toNegMemClass` `NegMemClass.neg_mem` `IntermediateField.mem_adjoin_simple_self` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `SubfieldClass.toInvMemClass` `InvMemClass.inv_mem` `induction3`
`isSolvable'` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsSolvableByRad`	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	—	`minpoly.eq_of_irreducible` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsScalarTower.left` `minpoly.algebraMap_eq` `IntermediateField.isScalarTower_mid'` `RingHom.injective` `DivisionRing.isSimpleRing` `isSolvable` `solvable_of_surjective` `Polynomial.Gal.restrictDvd_surjective` `mul_ne_zero_iff` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.C_eq_zero` `inv_eq_zero` `Irreducible.ne_zero` `Polynomial.leadingCoeff_ne_zero`

---

← Back to Index