PolynomialGaloisGroup

📁 Source: Mathlib/FieldTheory/PolynomialGaloisGroup.lean

Statistics

Metric	Count
Definitions `applyMulSemiringAction`, `galAction`, `galActionAux`, `galActionHom`, `instAlgebraSplittingFieldOfFactSplitsMapAlgebraMap`, `instUniqueOfFactSplits`, `mapRoots`, `restrict`, `restrictComp`, `restrictDvd`, `restrictProd`, `rootsEquivRoots`, `smul`, `uniqueGalC`, `uniqueGalOfSplits`, `uniqueGalOne`, `uniqueGalX`, `uniqueGalXPow`, `uniqueGalXSubC`, `uniqueGalZero`, `instAlgEquivClassGalSplittingField`, `instEquivLikeGalSplittingField`, `instFintypeGal`, `instGroupGal`	24
Theorems `card_of_separable`, `ext`, `ext_iff`, `galActionHom_injective`, `galActionHom_restrict`, `galAction_isPretransitive`, `instIsScalarTowerSplittingField`, `mapRoots_bijective`, `mul_splits_in_splittingField_of_mul`, `prime_degree_dvd_card`, `restrictComp_surjective`, `restrictDvd_def`, `restrictDvd_surjective`, `restrictProd_injective`, `restrict_smul`, `restrict_surjective`, `smul_def`, `splits_in_splittingField_of_comp`	18
Total	42

Polynomial

Definitions

Name	Category	Theorems
`instAlgEquivClassGalSplittingField` 📖	CompOp	—
`instEquivLikeGalSplittingField` 📖	CompOp	1 math math: `Gal.ext_iff`
`instFintypeGal` 📖	CompOp	—
`instGroupGal` 📖	CompOp	26 math math: `Gal.galActionHom_restrict`, `Gal.galActionHom_bijective_of_prime_degree'`, `Gal.smul_def`, `Gal.restrict_smul`, `Gal.galActionHom_injective`, `gal_X_pow_isSolvable`, `Gal.restrictDvd_def`, `solvableByRad.isSolvable'`, `gal_X_pow_sub_C_isSolvable`, `solvableByRad.isSolvable`, `gal_X_pow_sub_C_isSolvable_aux`, `gal_X_pow_sub_one_isSolvable`, `Gal.restrictComp_surjective`, `gal_C_isSolvable`, `gal_X_sub_C_isSolvable`, `gal_one_isSolvable`, `Gal.restrict_surjective`, `gal_mul_isSolvable`, `Gal.galActionHom_bijective_of_prime_degree`, `gal_zero_isSolvable`, `Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv`, `gal_isSolvable_of_splits`, `Gal.restrictProd_injective`, `Gal.restrictDvd_surjective`, `gal_X_isSolvable`, `gal_isSolvable_tower`

Polynomial.Gal

Definitions

Name	Category	Theorems
`applyMulSemiringAction` 📖	CompOp	—
`galAction` 📖	CompOp	—
`galActionAux` 📖	CompOp	1 math math: `smul_def`
`galActionHom` 📖	CompOp	5 math math: `galActionHom_restrict`, `galActionHom_bijective_of_prime_degree'`, `galActionHom_injective`, `galActionHom_bijective_of_prime_degree`, `card_complex_roots_eq_card_real_add_card_not_gal_inv`
`instAlgebraSplittingFieldOfFactSplitsMapAlgebraMap` 📖	CompOp	1 math math: `instIsScalarTowerSplittingField`
`instUniqueOfFactSplits` 📖	CompOp	—
`mapRoots` 📖	CompOp	1 math math: `mapRoots_bijective`
`restrict` 📖	CompOp	5 math math: `galActionHom_restrict`, `restrict_smul`, `restrictDvd_def`, `restrict_surjective`, `card_complex_roots_eq_card_real_add_card_not_gal_inv`
`restrictComp` 📖	CompOp	1 math math: `restrictComp_surjective`
`restrictDvd` 📖	CompOp	2 math math: `restrictDvd_def`, `restrictDvd_surjective`
`restrictProd` 📖	CompOp	1 math math: `restrictProd_injective`
`rootsEquivRoots` 📖	CompOp	1 math math: `smul_def`
`smul` 📖	CompOp	3 math math: `smul_def`, `restrict_smul`, `galAction_isPretransitive`
`uniqueGalC` 📖	CompOp	—
`uniqueGalOfSplits` 📖	CompOp	—
`uniqueGalOne` 📖	CompOp	—
`uniqueGalX` 📖	CompOp	—
`uniqueGalXPow` 📖	CompOp	—
`uniqueGalXSubC` 📖	CompOp	—
`uniqueGalZero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_of_separable` 📖	mathematical	`Polynomial.Separable` `Semifield.toCommSemiring` `Field.toSemifield`	`Nat.card` `Polynomial.Gal` `Module.finrank` `Polynomial.SplittingField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.instCommRingSplittingField` `Algebra.toModule` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	—	`IsGalois.card_aut_eq_finrank` `Polynomial.IsSplittingField.instFiniteDimensionalSplittingField` `IsGalois.of_separable_splitting_field` `Polynomial.IsSplittingField.splittingField`
`ext` 📖	—	`DFunLike.coe` `Polynomial.Gal` `Polynomial.SplittingField` `EquivLike.toFunLike` `Polynomial.instEquivLikeGalSplittingField`	—	—	`instIsDomain` `AlgEquiv.ext` `AlgHom.algHomClass` `AlgHom.mem_equalizer` `SetLike.ext_iff` `eq_top_iff` `Polynomial.SplittingField.adjoin_rootSet` `Algebra.adjoin_le_iff` `Algebra.mem_top`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `Polynomial.Gal` `Polynomial.SplittingField` `EquivLike.toFunLike` `Polynomial.instEquivLikeGalSplittingField`	—	`instIsDomain` `ext`
`galActionHom_injective` 📖	mathematical	—	`Polynomial.Gal` `Equiv.Perm` `Set.Elem` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `galActionHom`	—	`instIsDomain` `injective_iff_map_eq_one` `MonoidHom.instMonoidHomClass` `ext` `Equiv.Perm.ext_iff` `Equiv.injective` `Equiv.symm_apply_apply`
`galActionHom_restrict` 📖	mathematical	—	`Set` `Set.instMembership` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `DFunLike.coe` `Equiv.Perm` `Set.Elem` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom` `Polynomial.Gal` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `Equiv.Perm.permGroup` `MonoidHom.instFunLike` `galActionHom` `AlgEquiv` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.aut` `restrict` `AlgEquiv.instFunLike`	—	`instIsDomain` `restrict_smul`
`galAction_isPretransitive` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring`	`MulAction.IsPretransitive` `Polynomial.Gal` `Set.Elem` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `smul`	—	`instIsDomain` `minpoly.eq_of_irreducible` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.mem_rootSet` `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField` `Normal.minpoly_eq_iff_mem_orbit` `Polynomial.SplittingField.instNormal` `Equiv.apply_eq_iff_eq_symm_apply`
`instIsScalarTowerSplittingField` 📖	mathematical	—	`IsScalarTower` `Polynomial.SplittingField` `Polynomial.SplittingField.instSMulOfIsScalarTower` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsScalarTower.right` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toSMul` `Polynomial.SplittingField.instField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instAlgebraSplittingFieldOfFactSplitsMapAlgebraMap`	—	`IsScalarTower.of_algebraMap_eq` `Polynomial.IsSplittingField.splittingField` `Fact.out` `AlgHom.commutes`
`mapRoots_bijective` 📖	mathematical	—	`Function.Bijective` `Set.Elem` `Polynomial.SplittingField` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.instCommRingSplittingField` `instIsDomain` `Field.toSemifield` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `mapRoots`	—	`instIsDomain` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsScalarTowerSplittingField` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.Splits.roots_map` `Polynomial.IsSplittingField.splits` `Polynomial.IsSplittingField.splittingField` `Subtype.mem` `AlgHom.comp_algebraMap` `Polynomial.map_map` `Multiset.mem_toFinset`
`mul_splits_in_splittingField_of_mul` 📖	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`	`Polynomial` `Polynomial.instMul`	—	`Polynomial.map_mul` `Polynomial.Splits.mul` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `mul_ne_zero` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `Polynomial.map_dvd_map'` `dvd_mul_right` `AlgHom.comp_algebraMap` `Polynomial.map_map` `Polynomial.Splits.map` `dvd_mul_left`
`prime_degree_dvd_card` 📖	mathematical	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Nat.Prime` `Polynomial.natDegree`	`Nat.card` `Polynomial.Gal`	—	`card_of_separable` `Irreducible.separable` `Nat.Prime.ne_zero` `Polynomial.natDegree_eq_zero_iff_degree_le_zero` `le_of_eq` `Polynomial.SplittingField.splits` `Polynomial.degree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `IsIntegral.of_finite` `Polynomial.IsSplittingField.instFiniteDimensionalSplittingField` `minpoly.dvd` `Polynomial.eval_map_algebraMap` `Polynomial.eval_rootOfSplits` `Irreducible.dvd_symm` `minpoly.irreducible` `instIsDomain` `le_antisymm` `Polynomial.natDegree_le_of_dvd` `IsDomain.to_noZeroDivisors` `Irreducible.ne_zero` `minpoly.ne_zero` `Module.finrank_mul_finrank` `IntermediateField.isScalarTower_mid'` `commRing_strongRankCondition` `SubsemiringClass.nontrivial` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `IntermediateField.instSubfieldClass` `Module.Free.of_divisionRing` `IsScalarTower.left` `IntermediateField.adjoin.finrank`
`restrictComp_surjective` 📖	mathematical	—	`Polynomial.Gal` `Polynomial.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `MonoidHom.instFunLike` `restrictComp`	—	`restrict_surjective` `Polynomial.SplittingField.instNormal`
`restrictDvd_def` 📖	mathematical	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`restrictDvd` `MonoidHom` `AlgEquiv` `Polynomial.SplittingField` `Semifield.toCommSemiring` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `Algebra.id` `Polynomial.Gal` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Polynomial.instGroupGal` `Polynomial.instZero` `instOneMonoidHom` `restrict` `Polynomial.Splits` `Polynomial.map` `CommSemiring.toSemiring` `algebraMap` `Polynomial.Splits.of_dvd` `Polynomial.instCommRingSplittingField` `instIsDomain` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.toRing` `Field.toDivisionRing` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_dvd_map'`	—	`Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_dvd_map'`
`restrictDvd_surjective` 📖	mathematical	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Polynomial.Gal` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `MonoidHom.instFunLike` `restrictDvd`	—	`Polynomial.Splits.of_dvd` `instIsDomain` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_dvd_map'` `restrictDvd_def` `restrict_surjective` `Polynomial.SplittingField.instNormal`
`restrictProd_injective` 📖	mathematical	—	`Polynomial.Gal` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `Prod.instMulOneClass` `MonoidHom.instFunLike` `restrictProd`	—	`Unique.eq_default` `ext` `instIsDomain` `Multiset.mem_add` `Multiset.mem_toFinset` `Polynomial.aroots_mul` `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField` `Polynomial.rootSet_def` `Polynomial.Splits.of_dvd` `Polynomial.SplittingField.splits` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.map_dvd_map'` `dvd_mul_right` `Equiv.apply_symm_apply` `instIsScalarTowerSplittingField` `Polynomial.SplittingField.instNormal` `AlgEquiv.restrictNormal_commutes` `AlgEquiv.ext_iff` `restrictDvd_def` `dvd_mul_left`
`restrict_smul` 📖	mathematical	—	`Set` `Set.instMembership` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial.Gal` `Set.Elem` `smul` `DFunLike.coe` `MonoidHom` `AlgEquiv` `Semifield.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Polynomial.instGroupGal` `MonoidHom.instFunLike` `restrict` `AlgEquiv.instFunLike`	—	`instIsDomain` `instIsScalarTowerSplittingField` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.SplittingField.instNormal` `AlgEquiv.apply_symm_apply` `Equiv.apply_symm_apply`
`restrict_surjective` 📖	mathematical	—	`AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.Gal` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `Polynomial.instGroupGal` `MonoidHom.instFunLike` `restrict`	—	`AlgEquiv.restrictNormalHom_surjective` `instIsScalarTowerSplittingField` `Polynomial.SplittingField.instNormal`
`smul_def` 📖	mathematical	—	`Polynomial.Gal` `Set.Elem` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `smul` `DFunLike.coe` `Equiv` `Polynomial.SplittingField` `Polynomial.instCommRingSplittingField` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `EquivLike.toFunLike` `Equiv.instEquivLike` `rootsEquivRoots` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Polynomial.instGroupGal` `MulAction.toSemigroupAction` `galActionAux` `Equiv.symm`	—	`instIsDomain`
`splits_in_splittingField_of_comp` 📖	mathematical	—	`Polynomial.Splits` `Polynomial.SplittingField` `Polynomial.comp` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.SplittingField.instField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	—	`Polynomial.Splits.of_natDegree_le_one` `LE.le.trans` `Polynomial.natDegree_map_le` `Eq.trans_le` `zero_le_one` `Nat.instZeroLEOneClass` `Polynomial.Splits.exists_eval_eq_zero` `Polynomial.SplittingField.splits` `mul_eq_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `Polynomial.natDegree_comp` `IsDomain.to_noZeroDivisors` `instIsDomain` `Polynomial.natDegree_eq_of_degree_eq_some` `Polynomial.degree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.SplittingField.instNormal` `Normal.isIntegral` `Polynomial.Splits.of_dvd` `Normal.splits` `Polynomial.map_ne_zero` `minpoly.ne_zero` `Polynomial.map_dvd_map'` `Irreducible.dvd_symm` `minpoly.irreducible` `minpoly.dvd` `Polynomial.aeval_comp` `Polynomial.eval_map_algebraMap` `Polynomial.comp_eq_zero_iff` `MulZeroClass.zero_mul` `Polynomial.map_zero` `Polynomial.natDegree_C` `MulZeroClass.mul_zero` `mul_splits_in_splittingField_of_mul` `Polynomial.mul_comp` `WfDvdMonoid.induction_on_irreducible` `UniqueFactorizationMonoid.toIsWellFounded` `Polynomial.uniqueFactorizationMonoid` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `EuclideanDomain.to_principal_ideal_domain` `Polynomial.Splits.map` `IsUnit.splits`

---

← Back to Index