Documentation Verification Report

IsSplittingField

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

Statistics

Metric	Count
Definitions `IsSplittingField`	1
Theorems `adjoin_rootSet_isSplittingField`, `isSplittingField_iff`, `splits_iff_mem`, `splits_of_splits`, `mem_intermediateField_of_minpoly_splits`, `isAlgebraic`, `splits`, `adjoin_rootSet`, `adjoin_rootSet'`, `adjoin_rootSet_eq_range`, `finiteDimensional`, `map`, `mul`, `of_algEquiv`, `splits`, `splits'`, `splits_iff`, `isSplittingField_C`, `isSplittingField_iff_intermediateField`	19
Total	20

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rootSet_isSplittingField` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	`Polynomial.IsSplittingField` `IntermediateField` `SetLike.instMembership` `instSetLike` `adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `toField` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`instIsDomain` `IsScalarTower.left` `isSplittingField_iff` `splits_of_splits` `subset_adjoin`
`isSplittingField_iff` 📖	mathematical	—	`Polynomial.IsSplittingField` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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` `Polynomial.Splits` `Polynomial.map` `algebraMap` `adjoin` `Polynomial.rootSet` `instIsDomain`	—	`IsScalarTower.left` `instIsDomain` `toSubalgebra_injective` `adjoin_toSubalgebra_of_isAlgebraic` `isAlgebraic_of_mem_rootSet` `Polynomial.Splits.adjoin_rootSet_eq_range` `DivisionRing.isSimpleRing` `range_val` `Polynomial.IsSplittingField.splits'` `Polynomial.IsSplittingField.adjoin_rootSet'`
`splits_iff_mem` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	`IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `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`	—	`IsScalarTower.left` `instIsDomain` `Polynomial.Splits.image_rootSet` `DivisionRing.isSimpleRing` `Set.forall_mem_image` `splits_of_splits`
`splits_of_splits` 📖	mathematical	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `IntermediateField` `SetLike.instMembership` `instSetLike`	`toField` `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`	—	`instIsDomain` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsScalarTower.left` `Polynomial.Splits.of_splits_map` `DivisionRing.isSimpleRing` `IsScalarTower.algebraMap_eq` `isScalarTower_mid'` `Polynomial.map_map` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.eval_map_algebraMap` `Polynomial.rootSet_def`

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_intermediateField_of_minpoly_splits` 📖	—	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `Polynomial.Splits` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IntermediateField.toField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `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` `Module.toDistribMulAction` `Algebra.toModule` `minpoly`	—	—	`IsScalarTower.left` `IntermediateField.fieldRange_val` `mem_range_algebraMap_of_minpoly_splits` `IntermediateField.isScalarTower_mid'`

Polynomial

Definitions

Name	Category	Theorems
`IsSplittingField` 📖	CompData	21 math math: `IsSplittingField.mul`, `isSplittingField_X_pow_sub_C_of_root_adjoin_eq_top`, `FiniteField.instIsSplittingFieldExtensionHSubPolynomialHPowNatXCard`, `IsCyclotomicExtension.isSplittingField_X_pow_sub_one`, `IsGalois.is_separable_splitting_field`, `FiniteField.isSplittingField_of_nat_card_eq`, `Normal.exists_isSplittingField`, `IsSplittingField.splittingField`, `FiniteField.isSplittingField_of_card_eq`, `SplittingFieldAux.instIsSplittingFieldNatDegree`, `isSplittingField_AdjoinRoot_X_pow_sub_C`, `isSplittingField_C`, `IntermediateField.isSplittingField_iff`, `IsCyclotomicExtension.splitting_field_cyclotomic`, `FiniteField.isSplittingField_sub`, `IsSplittingField.of_algEquiv`, `IsGalois.tfae`, `isSplittingField_iff_intermediateField`, `IsSplittingField.map`, `isCyclic_tfae`, `IntermediateField.adjoin_rootSet_isSplittingField`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSplittingField_C` 📖	mathematical	—	`IsSplittingField` `Algebra.id` `Semifield.toCommSemiring` `Field.toSemifield` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C`	—	`map_C` `instIsDomain` `rootSet_C` `Algebra.adjoin_empty` `Subalgebra.bot_eq_top_of_finrank_eq_one` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Free.self` `Module.finrank_self`

Polynomial.IsSplittingField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adjoin_rootSet` 📖	mathematical	—	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `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`	—	`adjoin_rootSet'`
`adjoin_rootSet'` 📖	mathematical	—	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `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`	—	—
`adjoin_rootSet_eq_range` 📖	mathematical	—	`Algebra.adjoin` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `AlgHom.range`	—	`instIsDomain` `Polynomial.Splits.adjoin_rootSet_eq_range` `DivisionRing.isSimpleRing` `splits` `adjoin_rootSet`
`finiteDimensional` 📖	mathematical	—	`FiniteDimensional` `Field.toDivisionRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Algebra.toModule` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`instIsDomain` `fg_adjoin_of_finite` `Finset.finite_toSet` `Polynomial.rootSet_zero` `IsAlgebraic.isIntegral` `Polynomial.mem_rootSet'` `adjoin_rootSet` `Algebra.top_toSubmodule`
`map` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap`	—	`Polynomial.map_map` `IsScalarTower.algebraMap_eq` `splits` `Subalgebra.restrictScalars_injective` `instIsDomain` `Polynomial.rootSet.eq_1` `Polynomial.aroots.eq_1` `Subalgebra.restrictScalars_top` `eq_top_iff` `adjoin_rootSet` `Algebra.adjoin_le_iff` `Algebra.subset_adjoin`
`mul` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.instMul`	—	`Polynomial.map_mul` `IsScalarTower.algebraMap_eq` `Polynomial.map_map` `Polynomial.Splits.mul` `Polynomial.Splits.map` `splits` `instIsDomain` `Polynomial.rootSet.eq_1` `Polynomial.aroots_mul` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `mul_ne_zero` `Polynomial.instNoZeroDivisors` `IsDomain.to_noZeroDivisors` `Multiset.toFinset_add` `Finset.coe_union` `IsScalarTower.subalgebra'` `IsScalarTower.right` `Algebra.adjoin_union_eq_adjoin_adjoin` `Polynomial.aroots_def` `Polynomial.Splits.roots_map` `DivisionRing.isSimpleRing` `Multiset.toFinset_map` `Finset.coe_image` `Algebra.adjoin_algebraMap` `adjoin_rootSet` `Algebra.map_top` `IsScalarTower.adjoin_range_toAlgHom` `Subalgebra.restrictScalars_top`
`of_algEquiv` 📖	mathematical	—	`Polynomial.IsSplittingField`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.comp_algebraMap` `Polynomial.map_map` `Polynomial.Splits.map` `splits` `instIsDomain` `AlgHom.range_eq_top` `AlgEquiv.surjective` `Polynomial.Splits.adjoin_rootSet_eq_range` `DivisionRing.isSimpleRing` `adjoin_rootSet`
`splits` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	—	`splits'`
`splits'` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap`	—	—
`splits_iff` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Top.top` `Subalgebra` `Semifield.toCommSemiring` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Bot.bot` `OrderBot.toBot` `BoundedOrder.toOrderBot`	—	`eq_bot_iff` `instIsDomain` `adjoin_rootSet` `Polynomial.rootSet.eq_1` `Polynomial.aroots.eq_1` `Polynomial.Splits.roots_map` `DivisionRing.isSimpleRing` `Algebra.adjoin_le_iff` `Finset.mem_image` `Finset.mem_coe` `Multiset.toFinset_map` `SetLike.mem_coe` `Subalgebra.algebraMap_mem` `Polynomial.map_id` `RingEquiv.toRingHom_refl` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `Algebra.bijective_algebraMap_iff` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `RingEquiv.self_trans_symm` `RingEquiv.toRingHom_trans` `Polynomial.map_map` `Polynomial.Splits.map` `splits`

Polynomial.IsSplittingField.IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Polynomial.IsSplittingField.finiteDimensional` `Algebra.IsAlgebraic.trans` `IsDomain.to_noZeroDivisors` `instIsDomain` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`splits` 📖	mathematical	—	`Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.mapAlg`	—	`Polynomial.mapAlg_comp` `Polynomial.mapAlg_eq_map` `Polynomial.IsSplittingField.splits`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isSplittingField_iff_intermediateField` 📖	mathematical	—	`Polynomial.IsSplittingField` `Polynomial.Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `IntermediateField.adjoin` `Polynomial.rootSet` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Top.top` `IntermediateField` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `IntermediateField.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`instIsDomain` `IntermediateField.toSubalgebra_injective` `IntermediateField.adjoin_toSubalgebra_of_isAlgebraic` `isAlgebraic_of_mem_rootSet`

---

← Back to Index