Documentation Verification Report

AlgebraicClosure

📁 Source: Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Statistics

Metric	Count
Definitions `Monics`, `Vars`, `finEquivRoots`, `instAlgebra`, `instCommRing`, `instField`, `instGroupWithZero`, `instInhabited`, `instSMulOfIsScalarTower`, `maxIdeal`, `spanCoeffs`, `subProdXSubC`, `toSplittingField`	13
Theorems `map_eq_prod`, `splits_finsetProd`, `instCharP`, `instCharZero`, `instIsAlgClosure`, `instIsAlgClosureOfIsAlgebraic`, `instIsScalarTower`, `isAlgClosed`, `isAlgebraic`, `le_maxIdeal`, `isMaximal`, `spanCoeffs_ne_top`, `toSplittingField_coeff`, `normal_algebraicClosure`, `normal_algebraicClosure`, `instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`	16
Total	29

AlgebraicClosure

Definitions

Name	Category	Theorems
`Monics` 📖	CompOp	1 math math: `Monics.map_eq_prod`
`Vars` 📖	CompOp	7 math math: `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `maxIdeal.isMaximal`, `instIsAlgClosureOfIsAlgebraic`, `instIsAlgClosure`, `le_maxIdeal`, `toSplittingField_coeff`, `Monics.map_eq_prod`
`finEquivRoots` 📖	CompOp	—
`instAlgebra` 📖	CompOp	34 math math: `Field.Emb.Cardinal.equivLim_coherence`, `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `SeparableClosure.isSepClosed`, `Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor`, `IntermediateField.AdjoinDouble.normal_algebraicClosure`, `Algebra.isGeometricallyReduced_iff`, `Field.Emb.Cardinal.succEquiv_coherence`, `Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `PadicAlgCl.norm_extends`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `Field.absoluteGaloisGroup.commutator_closure_isNormal`, `Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`, `instIsAlgClosureOfIsAlgebraic`, `SeparableClosure.hasEnoughRootsOfUnity_pow`, `Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `PadicAlgCl.spectralNorm_eq`, `Field.Emb.Cardinal.equivSucc_coherence`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `SeparableClosure.hasEnoughRootsOfUnity`, `instIsAlgClosure`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `PadicAlgCl.isAlgebraic`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `Monics.map_eq_prod`, `spectralNorm.eq_of_normalClosure`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure'`, `IntermediateField.AdjoinSimple.normal_algebraicClosure`, `Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `isAlgebraic`, `PadicAlgCl.coe_eq`, `Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1`
`instCommRing` 📖	CompOp	6 math math: `PadicComplex.coe_eq`, `Algebra.isGeometricallyReduced_iff`, `hasEnoughRootsOfUnity`, `Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`, `hasEnoughRootsOfUnity_pow`, `PadicComplexInt.integers`
`instField` 📖	CompOp	41 math math: `Field.Emb.Cardinal.equivLim_coherence`, `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `SeparableClosure.isSepClosed`, `PadicComplex.coe_eq`, `Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor`, `PadicComplex.norm_def`, `IntermediateField.AdjoinDouble.normal_algebraicClosure`, `Algebra.isGeometricallyReduced_iff`, `Field.Emb.Cardinal.succEquiv_coherence`, `Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `PadicAlgCl.norm_extends`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1`, `Field.absoluteGaloisGroup.commutator_closure_isNormal`, `Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct`, `instIsAlgClosureOfIsAlgebraic`, `instCharP`, `SeparableClosure.hasEnoughRootsOfUnity_pow`, `Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `PadicAlgCl.spectralNorm_eq`, `Field.Emb.Cardinal.equivSucc_coherence`, `instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `SeparableClosure.hasEnoughRootsOfUnity`, `instIsAlgClosure`, `Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `PadicAlgCl.isAlgebraic`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `Monics.map_eq_prod`, `spectralNorm.eq_of_normalClosure`, `Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure`, `spectralNorm.eq_of_normalClosure'`, `IntermediateField.AdjoinSimple.normal_algebraicClosure`, `Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `isAlgebraic`, `PadicAlgCl.coe_eq`, `isAlgClosed`, `Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure`, `Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1`, `instCharZero`, `PadicComplexInt.integers`
`instGroupWithZero` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instSMulOfIsScalarTower` 📖	CompOp	3 math math: `PadicAlgCl.instUniformContinuousConstSMulPadic`, `PadicComplex.instIsScalarTowerPadicPadicAlgCl`, `instIsScalarTower`
`maxIdeal` 📖	CompOp	6 math math: `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`, `maxIdeal.isMaximal`, `instIsAlgClosureOfIsAlgebraic`, `instIsAlgClosure`, `le_maxIdeal`, `Monics.map_eq_prod`
`spanCoeffs` 📖	CompOp	1 math math: `le_maxIdeal`
`subProdXSubC` 📖	CompOp	1 math math: `toSplittingField_coeff`
`toSplittingField` 📖	CompOp	1 math math: `toSplittingField_coeff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCharP` 📖	mathematical	—	`CharP` `AlgebraicClosure` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`charP_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instCharZero` 📖	mathematical	—	`CharZero` `AlgebraicClosure` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `instField`	—	`charZero_of_injective_algebraMap` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing`
`instIsAlgClosure` 📖	mathematical	—	`IsAlgClosure` `AlgebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `instAlgebra` `CommRing.toCommSemiring` `Algebra.id` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `instIsDomain` `Field.toSemifield` `Submodule.Quotient.addCommGroup` `MvPolynomial` `Vars` `Semifield.toCommSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `maxIdeal` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`IsAlgClosure.of_splits` `instIsDomain` `Algebra.IsAlgebraic.isIntegral` `isAlgebraic` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Ideal.instIsTwoSided_1` `Monics.map_eq_prod` `Polynomial.Splits.prod` `Polynomial.Splits.map` `Polynomial.Splits.X_sub_C`
`instIsAlgClosureOfIsAlgebraic` 📖	mathematical	—	`IsAlgClosure` `AlgebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `instAlgebra` `CommRing.toCommSemiring` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `CommSemiring.toSemiring` `instIsDomain` `Field.toSemifield` `Submodule.Quotient.addCommGroup` `MvPolynomial` `Vars` `Semifield.toCommSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `maxIdeal` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `isAlgClosed` `Algebra.IsAlgebraic.trans` `instIsScalarTower` `IsScalarTower.right` `IsDomain.to_noZeroDivisors` `isAlgebraic`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `AlgebraicClosure` `Algebra.toSMul` `CommSemiring.toSemiring` `instSMulOfIsScalarTower` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsScalarTower.right`	—	`Ideal.Quotient.isScalarTower` `MvPolynomial.isScalarTower`
`isAlgClosed` 📖	mathematical	—	`IsAlgClosed` `AlgebraicClosure` `instField`	—	`IsAlgClosure.isAlgClosed` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `instIsAlgClosure`
`isAlgebraic` 📖	mathematical	—	`Algebra.IsAlgebraic` `AlgebraicClosure` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing` `instField` `instAlgebra` `CommRing.toCommSemiring` `Algebra.id`	—	`IsIntegral.isAlgebraic` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `MvPolynomial.induction_on` `isIntegral_algebraMap` `IsIntegral.add` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsIntegral.mul` `Monics.map_eq_prod` `Polynomial.eval_prod` `Finset.prod_congr` `Polynomial.map_sub` `Polynomial.eval_sub` `Finset.prod_eq_zero` `Finset.mem_univ` `Polynomial.map_C` `Polynomial.eval_C` `Polynomial.map_X` `Polynomial.eval_X` `Sigma.eta` `sub_self`
`le_maxIdeal` 📖	mathematical	—	`Ideal` `MvPolynomial` `Vars` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `spanCoeffs` `maxIdeal`	—	`Ideal.exists_le_maximal` `spanCoeffs_ne_top`
`spanCoeffs_ne_top` 📖	—	—	—	—	`Ideal.ne_top_iff_one` `spanCoeffs.eq_1` `Ideal.span.eq_1` `Set.image_univ` `Finsupp.mem_span_image_iff_linearCombination` `zero_ne_one` `NeZero.one` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finset.sum_eq_zero` `smul_eq_mul` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `toSplittingField_coeff` `Finset.mem_image_of_mem` `MulZeroClass.mul_zero` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `Finsupp.sum.eq_1` `Finsupp.linearCombination_apply` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass`
`toSplittingField_coeff` 📖	mathematical	`Monics` `Finset` `Finset.instMembership`	`DFunLike.coe` `AlgHom` `MvPolynomial` `Vars` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.SplittingField` `Finset.prod` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `CommRing.toCommMonoid` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.Monic` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `Polynomial.SplittingField.instField` `MvPolynomial.algebra` `Algebra.id` `Polynomial.SplittingField.instAlgebra` `AlgHom.funLike` `toSplittingField` `Polynomial.coeff` `subProdXSubC` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.instCommRingSplittingField`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.map_sub` `Polynomial.map_prod` `Finset.prod_congr` `Polynomial.map_X` `Polynomial.map_C` `MvPolynomial.aeval_X` `instIsDomain` `Monics.splits_finsetProd` `Equiv.prod_comp` `Equiv.apply_symm_apply` `Finset.prod_coe_sort` `Finset.prod_eq_multiset_prod` `Multiset.map_map` `Multiset.map_toEnumFinset_fst` `Polynomial.map_map` `AlgHom.comp_algebraMap` `Polynomial.Splits.eq_prod_roots` `Polynomial.leadingCoeff_map` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.C_1` `one_mul` `sub_self` `Polynomial.coeff_zero`

AlgebraicClosure.Monics

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_eq_prod` 📖	mathematical	—	`Polynomial.map` `AlgebraicClosure` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgebraicClosure.instField` `algebraMap` `AlgebraicClosure.instAlgebra` `Algebra.id` `Polynomial` `Polynomial.Monic` `Finset.prod` `Polynomial.natDegree` `HasQuotient.Quotient` `MvPolynomial` `AlgebraicClosure.Vars` `Ideal` `Ring.toSemiring` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Ideal.instHasQuotient` `AlgebraicClosure.maxIdeal` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `CommRing.toCommMonoid` `Polynomial.commRing` `Ideal.Quotient.commRing` `Finset.univ` `Fin.fintype` `MvPolynomial.commSemiring` `Polynomial.instSub` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `MvPolynomial.X` `AlgebraicClosure.Monics`	—	`Polynomial.ext` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_comp_algebraMap` `Polynomial.map_map` `Polynomial.map_prod` `sub_eq_zero` `Polynomial.coeff_sub` `Polynomial.map_sub` `AlgebraicClosure.subProdXSubC.eq_1` `Polynomial.coeff_map` `Ideal.Quotient.eq_zero_iff_mem` `AlgebraicClosure.le_maxIdeal` `Ideal.subset_span`
`splits_finsetProd` 📖	mathematical	`AlgebraicClosure.Monics` `Finset` `Finset.instMembership`	`Polynomial.Splits` `Polynomial.SplittingField` `Finset.prod` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `CommRing.toCommMonoid` `Polynomial.commRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.Monic` `Polynomial.SplittingField.instField` `Polynomial.map` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `algebraMap` `Polynomial.SplittingField.instAlgebra` `Algebra.id`	—	`Polynomial.splits_prod_iff` `instIsDomain` `Polynomial.map_ne_zero` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.Monic.ne_zero` `Polynomial.map_prod` `Polynomial.SplittingField.splits`

AlgebraicClosure.maxIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal` 📖	mathematical	—	`Ideal.IsMaximal` `MvPolynomial` `AlgebraicClosure.Vars` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `AlgebraicClosure.maxIdeal`	—	`Ideal.exists_le_maximal` `AlgebraicClosure.spanCoeffs_ne_top`

IntermediateField

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic` 📖	mathematical	—	`IsAlgClosure` `AlgebraicClosure` `IntermediateField` `SetLike.instMembership` `instSetLike` `toField` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `CommRing.toCommSemiring` `algebra'` `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` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `Submodule.Quotient.addCommGroup` `MvPolynomial` `AlgebraicClosure.Vars` `CommRing.toRing` `MvPolynomial.instCommRingMvPolynomial` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `AlgebraicClosure.maxIdeal` `GroupWithZero.toNoZeroSMulDivisors` `DivisionSemiring.toGroupWithZero` `SubNegMonoid.toAddMonoid` `SubNegZeroMonoid.toSubNegMonoid` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddCommGroup.toAddCommMonoid`	—	`IsScalarTower.left` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `instIsDomain` `GroupWithZero.toNoZeroSMulDivisors` `AlgebraicClosure.isAlgClosed` `Algebra.IsAlgebraic.trans` `AlgebraicClosure.instIsScalarTower` `SubringClass.toSubsemiringClass` `SubfieldClass.toSubringClass` `instSubfieldClass` `IsScalarTower.right` `SubsemiringClass.noZeroDivisors` `IsDomain.to_noZeroDivisors` `AlgebraicClosure.isAlgebraic`

IntermediateField.AdjoinDouble

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_algebraicClosure` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Normal` `AlgebraicClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instInsert` `Set.instSingletonSet` `IntermediateField.toField` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `IntermediateField.algebra'` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IntermediateField.isAlgebraic_adjoin_pair` `IsAlgClosure.normal` `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`

IntermediateField.AdjoinSimple

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`normal_algebraicClosure` 📖	mathematical	`IsIntegral` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivisionRing.toRing` `Field.toDivisionRing`	`Normal` `AlgebraicClosure` `IntermediateField` `SetLike.instMembership` `IntermediateField.instSetLike` `IntermediateField.adjoin` `Set` `Set.instSingletonSet` `IntermediateField.toField` `AlgebraicClosure.instField` `AlgebraicClosure.instAlgebra` `Semifield.toCommSemiring` `Field.toSemifield` `IntermediateField.algebra'` `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` `Module.toDistribMulAction` `Algebra.toModule`	—	`IsScalarTower.left` `IntermediateField.isAlgebraic_adjoin_simple` `IsAlgClosure.normal` `IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic`

---

← Back to Index