AbelRuffini

📁 Source: Mathlib/FieldTheory/AbelRuffini.lean

Statistics

Metric	Count
Definitions `IsSolvableByRad`, `solvableByRad`	2
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`, `isAlgebraic_solvableByRad`, `isIntegral_of_mem_solvableByRad`, `isSolvable_gal_minpoly`, `isSolvable_gal_of_irreducible`, `induction`, `isIntegral`, `isSolvable`, `isSolvable'`, `rad_mem`, `solvableByRad_le`, `solvableByRad_le_algClosure`, `splits_X_pow_sub_one_of_X_pow_sub_C`	25
Total	27

(root)

Definitions

Name	Category	Theorems
`IsSolvableByRad` 📖	CompData	—
`solvableByRad` 📖	CompOp	4 math math: `solvableByRad_le`, `solvableByRad.rad_mem`, `solvableByRad_le_algClosure`, `isAlgebraic_solvableByRad`

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.toPow` `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.toPow` `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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Polynomial.instOne`	`IsSolvable` `Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `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` `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.toPow` `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` `algebraMap` `Semifield.toCommSemiring` `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`	`IsSolvable` `Polynomial.Gal` `Multiset.prod` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommRing.toCommMonoid` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.instGroupGal`	—	`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`
`isAlgebraic_solvableByRad` 📖	mathematical	—	`Subalgebra.IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `IntermediateField.toSubalgebra` `solvableByRad`	—	`mem_algebraicClosure_iff` `solvableByRad_le_algClosure`
`isIntegral_of_mem_solvableByRad` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad`	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`IsAlgebraic.isIntegral` `isAlgebraic_solvableByRad`
`isSolvable_gal_minpoly` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad`	`IsSolvable` `Polynomial.Gal` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.instGroupGal`	—	`solvableByRad.induction` `minpoly.eq_X_sub_C` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isSolvable_of_subsingleton` `Unique.instSubsingleton` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.subset_adjoin` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `solvableByRad.rad_mem`
`isSolvable_gal_of_irreducible` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `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`	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	—	`minpoly.eq_of_irreducible` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `isSolvable_gal_minpoly` `solvable_of_surjective` `Polynomial.Gal.restrictDvd_surjective` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.nontrivial` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`solvableByRad_le` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike`	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `solvableByRad`	—	`sInf_le`
`solvableByRad_le_algClosure` 📖	mathematical	—	`IntermediateField` `Preorder.toLE` `PartialOrder.toPreorder` `IntermediateField.instPartialOrder` `solvableByRad` `algebraicClosure`	—	`solvableByRad_le` `mem_algebraicClosure_iff` `Polynomial.leadingCoeff_eq_zero` `mul_one` `one_pow` `Polynomial.leadingCoeff_X_pow` `Polynomial.leadingCoeff_comp` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natDegree_X_pow` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.aeval_comp` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X`
`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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C`	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`induction` 📖	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `RingHom.instFunLike` `algebraMap` `algebraMap_mem` `IntermediateField` `IntermediateField.instSetLike` `AddSubmonoidWithOneClass.toOneMemClass` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `NonAssocRing.toNonAssocSemiring` `NonAssocCommRing.toNonAssocRing` `CommRing.toNonAssocCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `Field.toDivisionRing` `IntermediateField.instSubfieldClass` `IntermediateField.instSMulMemClass` `solvableByRad` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `Ring.toNonAssocRing` `DivisionRing.toRing` `SubsemiringClass.toAddSubmonoidClass` `Distrib.toMul` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `SubsemiringClass.toSubmonoidClass` `rad_mem` `SetLike.instMembership`	—	—	`algebraMap_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `IntermediateField.instSMulMemClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `rad_mem` `RingHom.map_one` `RingHom.map_zero` `isAlgebraic_solvableByRad` `solvableByRad_le`
`isIntegral` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad`	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`isIntegral_of_mem_solvableByRad`
`isSolvable` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad`	`IsSolvable` `Polynomial.Gal` `minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.instGroupGal`	—	`isSolvable_gal_minpoly`
`isSolvable'` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `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`	`IsSolvable` `Polynomial.Gal` `Polynomial.instGroupGal`	—	`isSolvable_gal_of_irreducible`
`rad_mem` 📖	mathematical	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `solvableByRad`	—	—

---

← Back to Index