Documentation Verification Report

Construction

📁 Source: Mathlib/FieldTheory/SplittingField/Construction.lean

Statistics

Metric	Count
Definitions `algEquiv`, `SplittingField`, `algEquivSplittingFieldAux`, `instAlgebra`, `instField`, `instGroupWithZero`, `instIsScalarTower`, `instSMulOfIsScalarTower`, `SplittingFieldAux`, `algebra`, `algebra'`, `algebra''`, `algebra'''`, `SplittingFieldAuxAux`, `factor`, `instAlgebraSplittingField`, `instCommRingSplittingField`, `instInhabitedSplittingField`, `instInhabitedSplittingFieldAux`, `removeFactor`	20
Theorems `instFiniteDimensionalSplittingField`, `instFiniteSplittingField`, `instIsTorsionFreeSplittingField`, `splittingField`, `adjoin_rootSet`, `instCharP`, `instCharZero`, `instExpChar`, `splits`, `adjoin_rootSet`, `algebraMap_succ`, `instIsSplittingFieldNatDegree`, `scalar_tower'`, `splits`, `succ`, `X_sub_C_mul_removeFactor`, `fact_irreducible_factor`, `factor_dvd_of_degree_ne_zero`, `factor_dvd_of_natDegree_ne_zero`, `factor_dvd_of_not_isUnit`, `irreducible_factor`, `isCoprime_iff_aeval_ne_zero`, `natDegree_removeFactor`, `natDegree_removeFactor'`	24
Total	44

Polynomial

Definitions

Name	Category	Theorems
`SplittingField` 📖	CompOp	19 math math: `Gal.smul_def`, `Gal.mapRoots_bijective`, `IsSplittingField.instFiniteSplittingField`, `Gal.restrictDvd_def`, `Gal.instIsScalarTowerSplittingField`, `SplittingField.instExpChar`, `SplittingField.splits`, `IsSplittingField.instIsTorsionFreeSplittingField`, `AlgebraicClosure.Monics.splits_finsetProd`, `IsSplittingField.splittingField`, `AlgebraicClosure.toSplittingField_coeff`, `Gal.splits_in_splittingField_of_comp`, `SplittingField.instCharZero`, `IsSplittingField.instFiniteDimensionalSplittingField`, `SplittingField.instCharP`, `Gal.ext_iff`, `Gal.card_of_separable`, `SplittingField.adjoin_rootSet`, `SplittingField.instNormal`
`SplittingFieldAux` 📖	CompOp	6 math math: `SplittingFieldAux.succ`, `SplittingFieldAux.algebraMap_succ`, `SplittingFieldAux.adjoin_rootSet`, `SplittingFieldAux.scalar_tower'`, `SplittingFieldAux.instIsSplittingFieldNatDegree`, `SplittingFieldAux.splits`
`SplittingFieldAuxAux` 📖	CompOp	—
`factor` 📖	CompOp	11 math math: `SplittingFieldAux.succ`, `SplittingFieldAux.algebraMap_succ`, `factor_dvd_of_natDegree_ne_zero`, `natDegree_removeFactor`, `factor_dvd_of_degree_ne_zero`, `SplittingFieldAux.scalar_tower'`, `fact_irreducible_factor`, `natDegree_removeFactor'`, `factor_dvd_of_not_isUnit`, `irreducible_factor`, `X_sub_C_mul_removeFactor`
`instAlgebraSplittingField` 📖	CompOp	—
`instCommRingSplittingField` 📖	CompOp	7 math math: `Gal.smul_def`, `Gal.mapRoots_bijective`, `Gal.restrictDvd_def`, `IsSplittingField.instIsTorsionFreeSplittingField`, `AlgebraicClosure.toSplittingField_coeff`, `Gal.card_of_separable`, `SplittingField.adjoin_rootSet`
`instInhabitedSplittingField` 📖	CompOp	—
`instInhabitedSplittingFieldAux` 📖	CompOp	—
`removeFactor` 📖	CompOp	6 math math: `SplittingFieldAux.succ`, `SplittingFieldAux.algebraMap_succ`, `natDegree_removeFactor`, `SplittingFieldAux.scalar_tower'`, `natDegree_removeFactor'`, `X_sub_C_mul_removeFactor`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_sub_C_mul_removeFactor` 📖	mathematical	—	`Polynomial` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `factor` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AdjoinRoot.instField` `fact_irreducible_factor` `Field.toCommRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AdjoinRoot.instCommRing` `instMul` `instSub` `DivisionRing.toRing` `Field.toDivisionRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `AdjoinRoot.root` `removeFactor` `map` `AdjoinRoot.of`	—	`fact_irreducible_factor` `factor_dvd_of_natDegree_ne_zero` `mul_divByMonic_eq_iff_isRoot` `IsRoot.def` `eval_map` `eval₂_mul` `AdjoinRoot.eval₂_root` `MulZeroClass.zero_mul`
`fact_irreducible_factor` 📖	mathematical	—	`Fact` `Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `factor`	—	`irreducible_factor`
`factor_dvd_of_degree_ne_zero` 📖	mathematical	—	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `factor`	—	`factor_dvd_of_not_isUnit` `degree_eq_zero_of_isUnit` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`factor_dvd_of_natDegree_ne_zero` 📖	mathematical	—	`Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `factor`	—	`factor_dvd_of_degree_ne_zero` `natDegree_eq_of_degree_eq_some`
`factor_dvd_of_not_isUnit` 📖	mathematical	`IsUnit` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `factor`	—	`dvd_zero` `factor.eq_1` `WfDvdMonoid.exists_irreducible_factor` `UniqueFactorizationMonoid.toIsWellFounded` `PrincipalIdealRing.to_uniqueFactorizationMonoid` `instIsDomainOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `instIsDomain` `EuclideanDomain.to_principal_ideal_domain`
`irreducible_factor` 📖	mathematical	—	`Irreducible` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `semiring` `factor`	—	`factor.eq_1` `irreducible_X` `instIsDomain`
`isCoprime_iff_aeval_ne_zero` 📖	mathematical	—	`IsCoprime` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `commSemiring` `Semifield.toCommSemiring`	—	`aeval_ne_zero_of_isCoprime` `IsDomain.toNontrivial` `isCoprime_of_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `instIsDomain` `Mathlib.Tactic.Contrapose.contrapose₃` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `not_and_or` `fact_irreducible_factor` `AdjoinRoot.aeval_eq` `dvd_mul_of_dvd_left` `factor_dvd_of_not_isUnit`
`natDegree_removeFactor` 📖	mathematical	—	`natDegree` `AdjoinRoot` `Field.toCommRing` `factor` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AdjoinRoot.instField` `fact_irreducible_factor` `removeFactor`	—	`fact_irreducible_factor` `removeFactor.eq_1` `natDegree_divByMonic` `monic_X_sub_C` `natDegree_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `natDegree_X_sub_C`
`natDegree_removeFactor'` 📖	mathematical	`natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`AdjoinRoot` `Field.toCommRing` `factor` `AdjoinRoot.instField` `fact_irreducible_factor` `removeFactor`	—	`fact_irreducible_factor` `natDegree_removeFactor`

Polynomial.IsSplittingField

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteDimensionalSplittingField` 📖	mathematical	—	`FiniteDimensional` `Polynomial.SplittingField` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Polynomial.SplittingField.instField` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	—	`finiteDimensional` `splittingField`
`instFiniteSplittingField` 📖	mathematical	—	`Finite` `Polynomial.SplittingField`	—	`Module.finite_of_finite` `instFiniteDimensionalSplittingField`
`instIsTorsionFreeSplittingField` 📖	mathematical	—	`Module.IsTorsionFree` `Polynomial.SplittingField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.instCommRingSplittingField` `Algebra.toModule` `Semifield.toCommSemiring` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors`
`splittingField` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial.SplittingField` `Polynomial.SplittingField.instField` `Polynomial.SplittingField.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id`	—	`of_algEquiv` `Polynomial.SplittingFieldAux.instIsSplittingFieldNatDegree`

Polynomial.SplittingField

Definitions

Name	Category	Theorems
`algEquivSplittingFieldAux` 📖	CompOp	—
`instAlgebra` 📖	CompOp	13 math math: `Polynomial.Gal.smul_def`, `Polynomial.Gal.mapRoots_bijective`, `Polynomial.Gal.restrictDvd_def`, `splits`, `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField`, `AlgebraicClosure.Monics.splits_finsetProd`, `Polynomial.IsSplittingField.splittingField`, `AlgebraicClosure.toSplittingField_coeff`, `Polynomial.Gal.splits_in_splittingField_of_comp`, `Polynomial.IsSplittingField.instFiniteDimensionalSplittingField`, `Polynomial.Gal.card_of_separable`, `adjoin_rootSet`, `instNormal`
`instField` 📖	CompOp	17 math math: `Polynomial.Gal.smul_def`, `Polynomial.Gal.mapRoots_bijective`, `Polynomial.Gal.restrictDvd_def`, `Polynomial.Gal.instIsScalarTowerSplittingField`, `instExpChar`, `splits`, `Polynomial.IsSplittingField.instIsTorsionFreeSplittingField`, `AlgebraicClosure.Monics.splits_finsetProd`, `Polynomial.IsSplittingField.splittingField`, `AlgebraicClosure.toSplittingField_coeff`, `Polynomial.Gal.splits_in_splittingField_of_comp`, `instCharZero`, `Polynomial.IsSplittingField.instFiniteDimensionalSplittingField`, `instCharP`, `Polynomial.Gal.card_of_separable`, `adjoin_rootSet`, `instNormal`
`instGroupWithZero` 📖	CompOp	—
`instIsScalarTower` 📖	CompOp	—
`instSMulOfIsScalarTower` 📖	CompOp	1 math math: `Polynomial.Gal.instIsScalarTowerSplittingField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rootSet` 📖	mathematical	—	`Algebra.adjoin` `Polynomial.SplittingField` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instField` `instAlgebra` `Algebra.id` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.instCommRingSplittingField` `instIsDomain` `CommRing.toCommSemiring` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Polynomial.IsSplittingField.adjoin_rootSet` `Polynomial.IsSplittingField.splittingField`
`instCharP` 📖	mathematical	—	`CharP` `Polynomial.SplittingField` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`charP_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instCharZero` 📖	mathematical	—	`CharZero` `Polynomial.SplittingField` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`charZero_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instExpChar` 📖	mathematical	—	`ExpChar` `Polynomial.SplittingField` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`expChar_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`splits` 📖	mathematical	—	`Polynomial.Splits` `Polynomial.SplittingField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `instAlgebra` `Algebra.id`	—	`Polynomial.IsSplittingField.splits` `Polynomial.IsSplittingField.splittingField`

Polynomial.SplittingFieldAux

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	4 math math: `algebraMap_succ`, `adjoin_rootSet`, `instIsSplittingFieldNatDegree`, `splits`
`algebra'` 📖	CompOp	—
`algebra''` 📖	CompOp	1 math math: `scalar_tower'`
`algebra'''` 📖	CompOp	2 math math: `algebraMap_succ`, `scalar_tower'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rootSet` 📖	mathematical	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Algebra.adjoin` `Polynomial.SplittingFieldAux` `Semifield.toCommSemiring` `field` `algebra` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`instIsDomain` `Algebra.eq_top_iff` `Subalgebra.range_le` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.rootSet_def` `Polynomial.aroots_def` `Polynomial.fact_irreducible_factor` `algebraMap_succ` `Polynomial.map_map` `Polynomial.X_sub_C_mul_removeFactor` `Polynomial.map_mul` `Polynomial.roots_mul` `Polynomial.map_sub` `Polynomial.map_X` `Polynomial.map_C` `Polynomial.roots_X_sub_C` `Multiset.toFinset_add` `Finset.coe_union` `Multiset.toFinset_singleton` `Finset.coe_singleton` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Algebra.adjoin_union_eq_adjoin_adjoin` `Set.image_singleton` `scalar_tower'` `Algebra.adjoin_algebraMap` `AdjoinRoot.adjoinRoot_eq_top` `Algebra.map_top` `IsScalarTower.adjoin_range_toAlgHom` `Polynomial.natDegree_removeFactor'` `Subalgebra.restrictScalars_top`
`algebraMap_succ` 📖	mathematical	—	`algebraMap` `Polynomial.SplittingFieldAux` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `field` `algebra` `RingHom.comp` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.factor` `Field.toCommRing` `AdjoinRoot.instField` `Polynomial.fact_irreducible_factor` `Polynomial.removeFactor` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `algebra'''` `AdjoinRoot.of`	—	—
`instIsSplittingFieldNatDegree` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial.SplittingFieldAux` `Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `field` `algebra`	—	`splits` `adjoin_rootSet`
`scalar_tower'` 📖	mathematical	—	`IsScalarTower` `AdjoinRoot` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.factor` `Polynomial.SplittingFieldAux` `Field.toCommRing` `AdjoinRoot.instField` `Polynomial.fact_irreducible_factor` `Polynomial.removeFactor` `AdjoinRoot.instSMulAdjoinRoot` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `IsScalarTower.right` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id` `Algebra.toSMul` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `field` `algebra'''` `algebra''`	—	`IsScalarTower.of_algebraMap_eq` `Polynomial.fact_irreducible_factor`
`splits` 📖	mathematical	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Polynomial.Splits` `Polynomial.SplittingFieldAux` `field` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `algebra`	—	`Polynomial.Splits.of_degree_le_one` `LE.le.trans` `Polynomial.degree_map_le` `le_trans` `Polynomial.degree_le_natDegree` `WithBot.coe_le_coe` `zero_le_one` `Nat.instZeroLEOneClass` `Polynomial.fact_irreducible_factor` `algebraMap_succ` `Polynomial.map_map` `Polynomial.X_sub_C_mul_removeFactor` `Polynomial.map_mul` `Polynomial.Splits.mul` `Polynomial.Splits.map` `Polynomial.Splits.X_sub_C` `Polynomial.natDegree_removeFactor'`
`succ` 📖	mathematical	—	`Polynomial.SplittingFieldAux` `AdjoinRoot` `Field.toCommRing` `Polynomial.factor` `AdjoinRoot.instField` `Polynomial.fact_irreducible_factor` `Polynomial.removeFactor`	—	—

---

← Back to Index