Documentation Verification Report

IsIntegrallyClosed

📁 Source: Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

Statistics

Metric	Count
Definitions `powerBasis'`, `IsIntegrallyClosed`, `ofAdjoinEqTop'`, `ofGenMemAdjoin'`, `equivAdjoin`, `instAlgebraSubtypeMemSubringSubalgebraIntegralClosure`, `instSMulSubtypeMemSubringSubalgebraIntegralClosure`	7
Theorems `powerBasis'_dim`, `powerBasis'_gen`, `unique`, `minpoly_smul`, `ofAdjoinEqTop'_dim`, `ofAdjoinEqTop'_gen`, `ofGenMemAdjoin'_dim`, `ofGenMemAdjoin'_gen`, `degree_le_of_ne_zero`, `isIntegral_iff_isUnit_leadingCoeff`, `isIntegral_iff_leadingCoeff_dvd`, `unique_of_degree_le_degree_minpoly`, `injective`, `coe_equivAdjoin`, `equivAdjoin_toAlgHom`, `instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure`, `isIntegrallyClosed_dvd`, `isIntegrallyClosed_dvd_iff`, `isIntegrallyClosed_eq_field_fractions`, `isIntegrallyClosed_eq_field_fractions'`, `ker_eval`, `ofSubring`, `prime_of_isIntegrallyClosed`	23
Total	30

Algebra.adjoin

Definitions

Name	Category	Theorems
`powerBasis'` 📖	CompOp	3 math math: `powerBasis'_dim`, `powerBasis'_minpoly_gen`, `powerBasis'_gen`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`powerBasis'_dim` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`PowerBasis.dim` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra.toRing` `Subalgebra.algebra` `powerBasis'` `Polynomial.natDegree` `minpoly`	—	—
`powerBasis'_gen` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`PowerBasis.gen` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `Subalgebra.toRing` `Subalgebra.algebra` `powerBasis'` `Set.instMembership` `SetLike.coe` `SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton`	—	`SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `powerBasis'.eq_1` `PowerBasis.map_gen` `AdjoinRoot.powerBasis'_gen` `minpoly.equivAdjoin.eq_1` `AlgEquiv.ofBijective_apply` `AdjoinRoot.Minpoly.toAdjoin.eq_1` `AdjoinRoot.liftAlgHom_root`

IsIntegrallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minpoly_smul` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`minpoly` `Algebra.toSMul` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Polynomial.scaleRoots`	—	`FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Polynomial.map_injective` `FaithfulSMul.algebraMap_injective` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.self` `minpoly.isIntegrallyClosed_eq_field_fractions` `Localization.isLocalization` `FractionRing.instNontrivial` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `IsIntegral.smul` `Polynomial.map_scaleRoots` `Algebra.smul_def` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsScalarTower.algebraMap_apply` `Polynomial.eq_of_monic_of_associated` `minpoly.monic` `IsIntegral.mul` `isIntegral_algebraMap` `IsIntegral.tower_top` `IsIntegral.map` `AlgHom.algHomClass` `associated_of_dvd_dvd` `Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd` `AddCancelMonoid.toIsCancelAdd` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsDomain` `minpoly.dvd` `Polynomial.scaleRoots_aeval_eq_zero` `minpoly.aeval` `IsDomain.to_noZeroDivisors` `Polynomial.scaleRoots_dvd_iff` `Polynomial.scaleRoots_mul` `mul_inv_cancel₀` `Polynomial.scaleRoots_one` `inv_mul_cancel_left₀` `RingHomClass.toMonoidWithZeroHomClass` `map_inv₀`

IsIntegrallyClosed.minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unique` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree`	`minpoly` `CommRing.toRing`	—	`eq_of_sub_eq_zero` `LE.le.not_gt` `minpoly.IsIntegrallyClosed.degree_le_of_ne_zero` `Polynomial.aeval_sub` `minpoly.aeval` `sub_self` `Polynomial.degree_sub_lt` `le_antisymm` `minpoly.min` `minpoly.monic` `minpoly.ne_zero` `IsDomain.toNontrivial` `Polynomial.Monic.leadingCoeff`

PowerBasis

Definitions

Name	Category	Theorems
`ofAdjoinEqTop'` 📖	CompOp	4 math math: `ofAdjoinEqTop'_dim`, `ofGenMemAdjoin'_dim`, `ofAdjoinEqTop'_gen`, `ofGenMemAdjoin'_gen`
`ofGenMemAdjoin'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofAdjoinEqTop'_dim` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`dim` `ofAdjoinEqTop'` `Polynomial.natDegree` `minpoly`	—	—
`ofAdjoinEqTop'_gen` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`gen` `ofAdjoinEqTop'`	—	`SetLike.mem_coe` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin.powerBasis'_gen`
`ofGenMemAdjoin'_dim` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`dim` `ofAdjoinEqTop'` `Polynomial.natDegree` `minpoly`	—	`ofAdjoinEqTop'_dim`
`ofGenMemAdjoin'_gen` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Algebra.adjoin` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Set` `Set.instSingletonSet` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	`gen` `ofAdjoinEqTop'`	—	`ofAdjoinEqTop'_gen`

(root)

Definitions

Name	Category	Theorems
`IsIntegrallyClosed` 📖	MathDef	27 math math: `integralClosure.isIntegrallyClosedOfFiniteExtension`, `Valuation.Integers.isIntegrallyClosed`, `IsDedekindDomainDvr.isIntegrallyClosed`, `Valuation.Integers.integrallyClosed`, `Valuation.Integers.isIntegrallyClosed_integers`, `instIsIntegrallyClosedSubtypeMemValuationSubring`, `IsIntegrallyClosed.of_isIntegrallyClosed_of_isIntegrallyClosedIn`, `FunctionField.ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial`, `IsIntegrallyClosed.integralClosure_eq_bot_iff`, `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain`, `Field.instIsIntegrallyClosed`, `instIsIntegrallyClosedPolynomialOfIsDomain`, `Ring.instIsIntegrallyClosedNormalClosure`, `IsIntegrallyClosed.of_equiv`, `IsDedekindDomainInv.integrallyClosed`, `GCDMonoid.toIsIntegrallyClosed`, `IsDiscreteValuationRing.TFAE`, `isIntegrallyClosed_iff_isIntegrallyClosedIn`, `NumberField.RingOfIntegers.instIsIntegrallyClosed`, `isIntegrallyClosed_iff`, `Polynomial.isIntegrallyClosed_iff'`, `Subring.isIntegrallyClosed_iff`, `UniqueFactorizationMonoid.instIsIntegrallyClosed`, `IsIntegrallyClosed.of_isIntegrallyClosedIn`, `isIntegrallyClosed_iff_isIntegralClosure`, `isIntegrallyClosed_of_isLocalization`, `instIsIntegrallyClosedSubtypeMemSubring`

minpoly

Definitions

Name	Category	Theorems
`equivAdjoin` 📖	CompOp	2 math math: `equivAdjoin_toAlgHom`, `coe_equivAdjoin`
`instAlgebraSubtypeMemSubringSubalgebraIntegralClosure` 📖	CompOp	1 math math: `ofSubring`
`instSMulSubtypeMemSubringSubalgebraIntegralClosure` 📖	CompOp	1 math math: `instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_equivAdjoin` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`DFunLike.coe` `AlgEquiv` `AdjoinRoot` `minpoly` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `AdjoinRoot.instCommRing` `Subalgebra.toSemiring` `AdjoinRoot.instAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv.instFunLike` `equivAdjoin` `AlgHom` `AlgHom.funLike` `AdjoinRoot.Minpoly.toAdjoin`	—	—
`equivAdjoin_toAlgHom` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`AlgHomClass.toAlgHom` `AdjoinRoot` `minpoly` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `AdjoinRoot.instCommRing` `Subalgebra.toSemiring` `AdjoinRoot.instAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `equivAdjoin` `AdjoinRoot.Minpoly.toAdjoin`	—	`AlgEquivClass.toAlgHomClass` `AlgEquiv.instAlgEquivClass`
`instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure` 📖	mathematical	—	`IsScalarTower` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `Subalgebra` `CommRing.toCommSemiring` `Subring.toCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `CommSemiring.toSemiring` `Algebra.ofSubring` `Subalgebra.instSetLike` `integralClosure` `instSMulSubtypeMemSubringSubalgebraIntegralClosure` `Subalgebra.instSMulSubtypeMem` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `Algebra.id` `Subring.instSMulSubtypeMem` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	—	`IsScalarTower.subalgebra'` `IsScalarTower.right` `SubringClass.toSubsemiringClass` `Subring.instSubringClass`
`isIntegrallyClosed_dvd` 📖	mathematical	`IsIntegral` `CommRing.toRing` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Polynomial.commRing` `minpoly`	—	`FractionRing.instFaithfulSMul` `Module.IsTorsionFree.to_faithfulSMul` `IsDomain.toIsCancelMulZero` `IsDomain.toNontrivial` `Polynomial.map_modByMonic` `monic` `Polynomial.modByMonic_eq_sub_mul_div` `Polynomial.Monic.map` `dvd_sub` `dvd` `Polynomial.map_aeval_eq_aeval_map` `IsScalarTower.algebraMap_eq` `FractionRing.instIsScalarTower` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `IsScalarTower.left` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `dvd_mul_of_dvd_left` `isIntegrallyClosed_eq_field_fractions` `Localization.isLocalization` `FractionRing.instNontrivial` `dvd_refl` `Polynomial.modByMonic_eq_zero_iff_dvd` `Polynomial.eq_zero_of_dvd_of_degree_lt` `IsDomain.to_noZeroDivisors` `Polynomial.map_dvd_map` `IsFractionRing.injective` `Polynomial.degree_modByMonic_lt`
`isIntegrallyClosed_dvd_iff` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Polynomial.commRing` `minpoly`	—	`isIntegrallyClosed_dvd` `Polynomial.aeval_eq_zero_of_dvd_aeval_eq_zero` `aeval`
`isIntegrallyClosed_eq_field_fractions` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `Polynomial.map` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`eq_of_irreducible_of_monic` `Polynomial.Monic.irreducible_iff_irreducible_map_fraction_map` `monic` `irreducible` `Polynomial.aeval_map_algebraMap` `Polynomial.aeval_algebraMap_apply` `aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Polynomial.Monic.map`
`isIntegrallyClosed_eq_field_fractions'` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`minpoly` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Polynomial.map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `algebraMap`	—	`isIntegrallyClosed_eq_field_fractions` `FractionRing.instNontrivial` `IsDomain.toNontrivial` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `algebraMap_eq` `IsFractionRing.injective` `Localization.isLocalization`
`ker_eval` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`RingHom.ker` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `AlgHom.toRingHom` `Polynomial.algebraOfAlgebra` `Algebra.id` `Polynomial.aeval` `Ideal.span` `Set` `Set.instSingletonSet` `minpoly`	—	`Ideal.ext` `RingHom.instRingHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `isIntegrallyClosed_dvd_iff`
`ofSubring` 📖	mathematical	—	`Polynomial.map` `Subring` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `Subring.instSetLike` `CommSemiring.toSemiring` `SubsemiringClass.toCommSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `SubringClass.toSubsemiringClass` `Subring.instSubringClass` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `algebraMap` `Algebra.ofSubring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.id` `CommRing.toCommSemiring` `minpoly` `Subalgebra` `Subring.toCommRing` `Subalgebra.instSetLike` `integralClosure` `Subalgebra.toRing` `instAlgebraSubtypeMemSubringSubalgebraIntegralClosure`	—	`SubringClass.toSubsemiringClass` `Subring.instSubringClass` `isIntegrallyClosed_eq_field_fractions` `Subring.instIsDomainSubtypeMem` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Subring.instIsScalarTowerSubtypeMem` `IsScalarTower.left` `instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure` `instIsDomainSubtypeMemSubalgebraIntegralClosure` `IsIntegralClosure.isIntegral` `integralClosure.isIntegralClosure`
`prime_of_isIntegrallyClosed` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`Prime` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommSemiring.toCommMonoidWithZero` `Polynomial.commSemiring` `minpoly`	—	`Polynomial.Monic.ne_zero` `IsDomain.toNontrivial` `monic` `ne_of_lt` `degree_pos` `Polynomial.degree_eq_zero_of_isUnit` `IsDomain.to_noZeroDivisors` `isIntegrallyClosed_dvd_iff` `eq_zero_of_ne_zero_of_mul_left_eq_zero` `Polynomial.aeval_mul`

minpoly.IsIntegrallyClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`degree_le_of_ne_zero` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `minpoly` `CommRing.toRing`	—	`Polynomial.degree_eq_natDegree` `minpoly.ne_zero` `IsDomain.toNontrivial` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Polynomial.natDegree_le_of_dvd` `IsDomain.to_noZeroDivisors` `minpoly.isIntegrallyClosed_dvd_iff`
`isIntegral_iff_isUnit_leadingCoeff` 📖	mathematical	`Irreducible` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `DFunLike.coe` `AlgHom` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`IsIntegral` `CommRing.toRing` `IsUnit` `Polynomial.leadingCoeff`	—	`minpoly.isIntegrallyClosed_dvd` `Polynomial.leadingCoeff_mul` `IsDomain.to_noZeroDivisors` `minpoly.monic` `one_mul` `IsUnit.map` `MonoidHom.instMonoidHomClass` `of_irreducible_mul` `minpoly.not_isUnit` `IsDomain.toNontrivial` `smul_smul` `IsUnit.val_inv_mul` `one_smul` `IsIntegral.smul` `IsScalarTower.left` `isIntegral_leadingCoeff_smul`
`isIntegral_iff_leadingCoeff_dvd` 📖	mathematical	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree`	`IsIntegral` `CommRing.toRing` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `Polynomial.commRing` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Polynomial.C` `Polynomial.leadingCoeff`	—	`minpoly.isIntegrallyClosed_dvd` `WithBot.le_of_add_le_add_left` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Polynomial.degree_ne_bot` `minpoly.ne_zero` `IsDomain.toNontrivial` `Polynomial.degree_mul` `IsDomain.to_noZeroDivisors` `add_zero` `minpoly.monic` `minpoly.aeval` `Polynomial.degree_le_zero_iff` `Polynomial.leadingCoeff_mul` `Polynomial.Monic.leadingCoeff` `Polynomial.leadingCoeff_C` `one_mul` `mul_comm` `minpoly.ne_zero_iff` `IsIntegrallyClosed.minpoly.unique` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_C` `Module.IsTorsionFree.to_faithfulSMul` `Polynomial.degree_C_mul` `right_ne_zero_of_mul`
`unique_of_degree_le_degree_minpoly` 📖	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.aeval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `WithBot` `Preorder.toLE` `WithBot.instPreorder` `Nat.instPreorder` `Polynomial.degree` `minpoly` `CommRing.toRing`	—	—	`IsIntegrallyClosed.minpoly.unique` `LE.le.trans` `minpoly.min`

minpoly.ToAdjoin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`AdjoinRoot` `minpoly` `Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `Algebra.adjoin` `Set` `Set.instSingletonSet` `DFunLike.coe` `AlgHom` `AdjoinRoot.instCommRing` `Subalgebra.toSemiring` `AdjoinRoot.instAlgebra` `Algebra.id` `Subalgebra.algebra` `AlgHom.funLike` `AdjoinRoot.Minpoly.toAdjoin`	—	`injective_iff_map_eq_zero` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `AdjoinRoot.mk_surjective` `Algebra.self_mem_adjoin_singleton` `AddSubmonoidClass.toZeroMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `Polynomial.coe_aeval_mk_apply` `minpoly.isIntegrallyClosed_dvd_iff`

---

← Back to Index