Basic

📁 Source: Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Statistics

Metric	Count
Definitions mapIntegralClosure, mapIntegralClosure, equiv, mk'	4
Theorems coe_mapIntegralClosure, coe_mapIntegralClosure, adjoin, finite, inv_mem, isField_iff_isField, isLocalHom, quotient, tower_bot, tower_top, trans, isIntegral, isIntegral', finite_iff_isIntegral_and_finiteType, isIntegral_iSup, isIntegral_sup, det, inv, inv_mem, inv_mem_adjoin, isUnit, mem_of_inv_mem, multiset_prod, multiset_sum, nsmul, of_mem_closure', of_mem_closure'', of_mul_unit, pow, pow_iff, prod, sum, tower_bot, tower_bot_of_field, zsmul, algebraMap_equiv, algebraMap_lift, algebraMap_mk', isField, isIntegral, isIntegral_algebra, isTorsionFree, mk'_add, mk'_algebraMap, mk'_mul, mk'_one, mk'_zero, tower_top, quotient_isIntegral, quotient_isIntegralElem, of_isIntegral_of_finiteType, isLocalHom, quotient, to_finite, tower_bot, tower_top, trans, of_mul_unit, finite_iff_isIntegral_and_finiteType, of_comp, isIntegralElem_leadingCoeff_mul, isIntegral_of_surjective, adjoin_le_integralClosure, instIsDomainSubtypeMemSubalgebraIntegralClosure, instIsIntegralMvPolynomial, instIsIntegralPolynomial, instIsIntegralQuotientIdeal, AlgebraIsIntegral, isIntegral, isIntegralClosure, integralClosure_eq_top_iff, integralClosure_idem, integralClosure_map_algEquiv, isField_of_isIntegral_of_isField, isField_of_isIntegral_of_isField', isIntegral_leadingCoeff_smul, isIntegral_quotientMap_iff, isIntegral_trans, le_integralClosure_iff_isIntegral, mem_integralClosure_iff_mem_fg, roots_mem_integralClosure	81
Total	85

AlgEquiv

Definitions

Name	Category	Theorems
mapIntegralClosure 📖	CompOp	1 math math: coe_mapIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mapIntegralClosure 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure DFunLike.coe AlgEquiv Subalgebra.toSemiring Subalgebra.algebra instFunLike mapIntegralClosure	—	—

AlgHom

Definitions

Name	Category	Theorems
mapIntegralClosure 📖	CompOp	1 math math: coe_mapIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mapIntegralClosure 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure DFunLike.coe AlgHom Subalgebra.toSemiring Subalgebra.algebra funLike mapIntegralClosure	—	—

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iff_isIntegral_and_finiteType 📖	mathematical	—	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing toModule IsIntegral CommRing.toRing FiniteType	—	IsIntegral.of_finite Module.Finite.finiteType IsIntegral.finite
isIntegral_iSup 📖	mathematical	—	IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subalgebra.toRing CommRing.toRing Subalgebra.algebra	—	—
isIntegral_sup 📖	mathematical	—	IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLatticeSubalgebra Subalgebra.toRing CommRing.toRing Subalgebra.algebra	—	—

Algebra.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin 📖	mathematical	IsIntegral CommRing.toRing	Algebra.IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Subalgebra.toRing Subalgebra.algebra	—	le_integralClosure_iff_isIntegral Algebra.adjoin_le
finite 📖	mathematical	—	Module.Finite CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	fg_adjoin_of_finite Finset.finite_toSet isIntegral
inv_mem 📖	mathematical	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	IsIntegral.inv_mem isIntegral_algHom_iff Subtype.val_injective isIntegral
isField_iff_isField 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	IsField	—	isField_of_isIntegral_of_isField' isField_of_isIntegral_of_isField
isLocalHom 📖	mathematical	—	IsLocalHom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap	—	RingHom.IsIntegral.isLocalHom algebraMap_isIntegral_iff FaithfulSMul.algebraMap_injective
quotient 📖	mathematical	—	Algebra.IsIntegral HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Ideal.Quotient.commRing Ideal.Quotient.instRingQuotient Ideal.instAlgebraQuotientComapRingHomAlgebraMap	—	RingHom.instRingHomClass RingHom.IsIntegral.quotient isIntegral
tower_bot 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	RingHom.IsIntegral.tower_bot FaithfulSMul.algebraMap_injective Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsScalarTower.algebraMap_eq isIntegral
tower_top 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	RingHom.IsIntegral.tower_top IsScalarTower.algebraMap_eq isIntegral
trans 📖	mathematical	—	Algebra.IsIntegral	—	isIntegral_trans isIntegral

Algebra.IsPushout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	isIntegral' symm
isIntegral' 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	Algebra.to_smulCommClass AlgEquiv.isIntegral_iff Algebra.IsIntegral.tensorProduct

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det 📖	mathematical	IsIntegral CommRing.toRing	Matrix.det	—	Matrix.det_apply sum zsmul prod
inv 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero DivisionRing.toDivisionSemiring	—	of_mem_of_fg fg_adjoin_singleton inv_mem_adjoin
inv_mem 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	Algebra.adjoin_le Set.singleton_subset_iff inv_mem_adjoin
inv_mem_adjoin 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing	Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	eq_or_ne inv_zero Subalgebra.zero_mem Module.Finite.of_fg fg_adjoin_singleton Algebra.subset_adjoin FiniteDimensional.exists_mul_eq_one Subalgebra.isDomain DivisionRing.isDomain mul_left_cancel₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero mul_inv_cancel₀
isUnit 📖	mathematical	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	Module.Finite.of_fg fg_adjoin_singleton IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.subset_adjoin FiniteDimensional.isUnit Subalgebra.isDomain
mem_of_inv_mem 📖	—	IsIntegral EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Subalgebra Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring SetLike.instMembership Subalgebra.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	—	inv_inv inv_mem inv
multiset_prod 📖	mathematical	IsIntegral CommRing.toRing	Multiset.prod CommRing.toCommMonoid	—	Subalgebra.multiset_prod_mem
multiset_sum 📖	mathematical	IsIntegral CommRing.toRing	Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Subalgebra.multiset_sum_mem
nsmul 📖	mathematical	IsIntegral	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	smul AddCommMonoid.nat_isScalarTower
of_mem_closure' 📖	—	IsIntegral CommRing.toRing Subring SetLike.instMembership Subring.instSetLike Subring.closure	—	—	Subring.closure_induction isIntegral_zero isIntegral_one add neg mul
of_mem_closure'' 📖	—	RingHom.IsIntegralElem CommRing.toRing Subring SetLike.instMembership Subring.instSetLike Subring.closure	—	—	of_mem_closure'
of_mul_unit 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne IsIntegral	—	—	Polynomial.monic_scaleRoots_iff Algebra.commutes mul_assoc mul_one Polynomial.scaleRoots_aeval_eq_zero
pow 📖	mathematical	IsIntegral	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	of_mem_of_fg fg_adjoin_singleton Subalgebra.pow_mem Algebra.subset_adjoin
pow_iff 📖	mathematical	—	IsIntegral CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	—	of_pow pow
prod 📖	mathematical	IsIntegral CommRing.toRing	Finset.prod CommRing.toCommMonoid	—	Subalgebra.prod_mem
sum 📖	mathematical	IsIntegral CommRing.toRing	Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Subalgebra.sum_mem
tower_bot 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap IsIntegral	CommRing.toRing	—	isIntegral_algHom_iff
tower_bot_of_field 📖	mathematical	IsIntegral DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield Ring.toSemiring RingHom.instFunLike algebraMap	DivisionRing.toRing Field.toDivisionRing	—	tower_bot RingHom.injective DivisionRing.isSimpleRing
zsmul 📖	mathematical	IsIntegral	SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	smul AddCommGroup.intIsScalarTower

IsIntegralClosure

Definitions

Name	Category	Theorems
equiv 📖	CompOp	4 math math: NumberField.RingOfIntegers.withValEquiv_symm_apply, algebraMap_equiv, NumberField.RingOfIntegers.withValEquiv_apply, Rat.ringOfIntegersWithValEquiv_apply
mk' 📖	CompOp	7 math math: mk'_add, mk'_zero, algebraMap_mk', mk'_algebraMap, mk'_mul, mk'_one, prod_galRestrict_eq_norm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_equiv 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap AlgEquiv AlgEquiv.instFunLike equiv	—	algebraMap_lift isIntegral_algebra
algebraMap_lift 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap AlgHom AlgHom.funLike lift	—	algebraMap_mk' IsIntegral.algebraMap Algebra.IsIntegral.isIntegral
algebraMap_mk' 📖	mathematical	IsIntegral CommRing.toRing	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap mk'	—	isIntegral_iff
isField 📖	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	—	isIntegral_algebra isField_of_isIntegral_of_isField'
isIntegral 📖	mathematical	—	IsIntegral CommRing.toRing	—	isIntegral_algebraMap_iff algebraMap_injective isIntegral_iff
isIntegral_algebra 📖	mathematical	—	Algebra.IsIntegral CommRing.toRing	—	isIntegral
isTorsionFree 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Function.Injective.moduleIsTorsionFree algebraMap_injective Algebra.algebraMap_eq_smul_one IsScalarTower.smul_assoc
mk'_add 📖	mathematical	IsIntegral CommRing.toRing	mk' Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsIntegral.add	—	algebraMap_injective IsIntegral.add algebraMap_mk' map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
mk'_algebraMap 📖	mathematical	IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap isIntegral_algebraMap	mk'	—	algebraMap_injective algebraMap_mk' IsScalarTower.algebraMap_apply
mk'_mul 📖	mathematical	IsIntegral CommRing.toRing	mk' Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsIntegral.mul	—	algebraMap_injective IsIntegral.mul algebraMap_mk' map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
mk'_one 📖	mathematical	IsIntegral CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne isIntegral_one	mk'	—	algebraMap_injective algebraMap_mk' map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
mk'_zero 📖	mathematical	IsIntegral CommRing.toRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing isIntegral_zero	mk'	—	algebraMap_injective algebraMap_mk' map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
tower_top 📖	mathematical	—	IsIntegralClosure	—	algebraMap_injective isIntegral_iff isIntegral_trans IsIntegral.tower_top

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotient_isIntegral 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial Ideal Polynomial.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	RingHom.IsIntegral HasQuotient.Quotient Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.instRingQuotient Polynomial.commRing AlgHom.toRingHom Ideal.Quotient.ring Ideal.instIsTwoSided_1 Algebra.id Ideal.Quotient.algebra Polynomial.algebraOfAlgebra AlgHom.comp Ideal.Quotient.mkₐ Algebra.ofId	—	Ideal.instIsTwoSided_1 Subalgebra.ext Ideal.Quotient.mkₐ_surjective Polynomial.aeval_eq_sum_range' lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.as_sum_range_C_mul_X_pow map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass IsScalarTower.right Finset.sum_congr Polynomial.C_mul' map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_mem_adjoin_singleton adjoin_le_integralClosure quotient_isIntegralElem Algebra.mem_top
quotient_isIntegralElem 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial Ideal Polynomial.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	RingHom.IsIntegralElem HasQuotient.Quotient Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.instRingQuotient Polynomial.commRing RingHom.comp Ideal.Quotient.ring Ideal.instIsTwoSided_1 algebraMap Polynomial.algebraOfAlgebra Algebra.id DFunLike.coe RingHom RingHom.instFunLike Polynomial.X	—	Ideal.instIsTwoSided_1 Ideal.Quotient.eq_zero_iff_mem Polynomial.eval₂_eq_sum_range Polynomial.as_sum_range_C_mul_X_pow Finset.sum_congr map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_iff_isIntegral_and_finiteType 📖	mathematical	—	Finite IsIntegral CommRing.toRing FiniteType	—	Finite.to_isIntegral Finite.to_finiteType IsIntegral.to_finite
isIntegralElem_leadingCoeff_mul 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsIntegralElem CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom Semiring.toNonAssocSemiring instFunLike Polynomial.leadingCoeff	—	Polynomial.natDegree_zero Polynomial.monic_integralNormalization Polynomial.integralNormalization_eval₂_leadingCoeff_mul MulZeroClass.mul_zero Polynomial.coeff_natDegree Polynomial.coeff_zero Polynomial.coeff_map MulZeroClass.zero_mul isIntegralElem_zero Polynomial.eq_C_of_natDegree_eq_zero Polynomial.map_C Polynomial.eval₂_C Polynomial.C_eq_zero
isIntegral_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instFunLike	IsIntegral CommRing.toRing	—	isIntegralElem_map

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isIntegral_of_finiteType 📖	mathematical	RingHom.IsIntegral CommRing.toRing	RingHom.Finite	—	RingHom.IsIntegral.to_finite

RingHom.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLocalHom 📖	mathematical	RingHom.IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	IsLocalHom MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	IsUnit.of_mul_eq_one instIsDedekindFiniteMonoid mul_neg Polynomial.eval_X Polynomial.eval_mul Polynomial.coeff_zero_reverse add_eq_zero_iff_neg_eq Polynomial.eval_C Polynomial.eval_add Polynomial.X_mul_divX_add injective_iff_map_eq_zero' RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.eval₂_hom Polynomial.eval₂_reverse_eq_zero_iff
quotient 📖	mathematical	RingHom.IsIntegral CommRing.toRing	HasQuotient.Quotient Ideal Ring.toSemiring Ideal.instHasQuotient Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass Ideal.Quotient.commRing Ideal.Quotient.instRingQuotient Ideal.quotientMap Ideal.instIsTwoSided_1 le_rfl PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	RingHom.instRingHomClass Ideal.instIsTwoSided_1 le_rfl Polynomial.Monic.map Polynomial.eval₂_map Polynomial.hom_eval₂
to_finite 📖	mathematical	RingHom.IsIntegral CommRing.toRing	RingHom.Finite	—	Algebra.IsIntegral.finite
tower_bot 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.IsIntegral CommRing.toRing RingHom.comp	—	—	IsIntegral.tower_bot IsScalarTower.of_algebraMap_eq
tower_top 📖	—	RingHom.IsIntegral CommRing.toRing RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—	RingHom.isIntegralElem.of_comp
trans 📖	mathematical	RingHom.IsIntegral CommRing.toRing	RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	IsScalarTower.of_algebraMap_eq Algebra.IsIntegral.trans Algebra.IsIntegral.isIntegral

RingHom.IsIntegralElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_mul_unit 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom.IsIntegralElem	—	—	IsIntegral.of_mul_unit

RingHom.isIntegralElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_comp 📖	—	RingHom.IsIntegralElem CommRing.toRing RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring	—	—	Polynomial.Monic.map Polynomial.eval₂_map

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_le_integralClosure 📖	mathematical	IsIntegral CommRing.toRing	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Algebra.adjoin Set Set.instSingletonSet integralClosure	—	Algebra.adjoin_le_iff
instIsDomainSubtypeMemSubalgebraIntegralClosure 📖	mathematical	—	IsDomain Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toSemiring	—	Subalgebra.isDomain
instIsIntegralMvPolynomial 📖	mathematical	—	Algebra.IsIntegral MvPolynomial CommRing.toCommSemiring MvPolynomial.instCommRingMvPolynomial CommRing.toRing MvPolynomial.algebraMvPolynomial	—	Algebra.IsPushout.isIntegral MvPolynomial.isScalarTower IsScalarTower.right MvPolynomial.instIsScalarTower MvPolynomial.instIsPushout
instIsIntegralPolynomial 📖	mathematical	—	Algebra.IsIntegral Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing Polynomial.ring CommRing.toRing Polynomial.algebra	—	Algebra.IsPushout.isIntegral Polynomial.isScalarTower IsScalarTower.right instIsScalarTowerPolynomial IsScalarTower.left instIsPushoutPolynomial
instIsIntegralQuotientIdeal 📖	mathematical	—	Algebra.IsIntegral HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.instRingQuotient Ideal.instAlgebraQuotient	—	Algebra.IsIntegral.trans Ideal.Quotient.isScalarTower IsScalarTower.right Algebra.IsIntegral.of_finite Module.Finite.quotient Module.Finite.self
integralClosure_eq_top_iff 📖	mathematical	—	integralClosure Top.top Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Algebra.IsIntegral CommRing.toRing	—	top_le_iff le_integralClosure_iff_isIntegral AlgEquiv.isIntegral_iff
integralClosure_idem 📖	mathematical	—	integralClosure Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Subalgebra.toCommRing Subalgebra.toAlgebra Algebra.id Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	eq_bot_iff Algebra.mem_bot isIntegral_trans IsScalarTower.subalgebra' IsScalarTower.right integralClosure.AlgebraIsIntegral
integralClosure_map_algEquiv 📖	mathematical	—	Subalgebra.map CommRing.toCommSemiring CommSemiring.toSemiring AlgHomClass.toAlgHom AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass integralClosure	—	Subalgebra.ext AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Subalgebra.mem_map IsIntegral.map IsScalarTower.left AlgHom.algHomClass AlgEquiv.apply_symm_apply
isField_of_isIntegral_of_isField 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap IsField	—	—	faithfulSMul_iff_algebraMap_injective IsLocalHom.isField RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Algebra.IsIntegral.isLocalHom
isField_of_isIntegral_of_isField' 📖	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	—	zero_ne_one NeZero.one IsDomain.toNontrivial mul_comm IsIntegral.isUnit Algebra.IsIntegral.isIntegral Units.val_inv
isIntegral_leadingCoeff_smul 📖	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	IsIntegral CommRing.toRing Algebra.toSMul Polynomial.leadingCoeff	—	Algebra.smul_def RingHom.isIntegralElem_leadingCoeff_mul Polynomial.aeval_def
isIntegral_quotientMap_iff 📖	mathematical	—	RingHom.IsIntegral HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass Ideal.Quotient.commRing Ideal.Quotient.instRingQuotient Ideal.quotientMap Ideal.instIsTwoSided_1 le_rfl PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.comp CommSemiring.toSemiring CommRing.toCommSemiring Ideal.Quotient.ring	—	RingHom.instRingHomClass Ideal.instIsTwoSided_1 le_rfl RingHom.IsIntegral.trans RingHom.isIntegral_of_surjective Ideal.Quotient.mk_surjective RingHom.IsIntegral.tower_top
isIntegral_trans 📖	—	IsIntegral	—	—	Submodule.fg_top fg_adjoin_of_finite Finset.finite_toSet Algebra.IsIntegral.isIntegral Algebra.subset_adjoin Polynomial.monic_toSubring IsScalarTower.algebraMap_eq IsScalarTower.subalgebra Polynomial.eval₂_map Polynomial.map_toSubring Submodule.addSubmonoidClass Submodule.smulMemClass Module.Finite.of_fg IsIntegral.fg_adjoin_singleton IsIntegral.of_mem_of_fg IsScalarTower.subalgebra' Module.Finite.iff_fg Submodule.isScalarTower Module.Finite.trans Subalgebra.mem_restrictScalars
le_integralClosure_iff_isIntegral 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder integralClosure Algebra.IsIntegral SetLike.instMembership Subalgebra.instSetLike Subalgebra.toRing CommRing.toRing Subalgebra.algebra	—	SetLike.forall isIntegral_algebraMap_iff IsScalarTower.subalgebra' IsScalarTower.right Subtype.coe_injective Algebra.isIntegral_def
mem_integralClosure_iff_mem_fg 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Submodule.FG NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule DFunLike.coe OrderEmbedding Submodule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule	—	IsIntegral.fg_adjoin_singleton Algebra.subset_adjoin IsIntegral.of_mem_of_fg
roots_mem_integralClosure 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Multiset Multiset.instMembership Polynomial.aroots	Subalgebra SetLike.instMembership Subalgebra.instSetLike integralClosure	—	Polynomial.eval₂_eq_eval_map Polynomial.mem_roots Polynomial.Monic.ne_zero IsDomain.toNontrivial Polynomial.Monic.map

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
AlgebraIsIntegral 📖	mathematical	—	Algebra.IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toRing CommRing.toRing Subalgebra.algebra	—	isIntegral
isIntegral 📖	mathematical	—	IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toRing CommRing.toRing Subalgebra.algebra	—	Polynomial.aeval_algHom_apply AlgHom.algHomClass Subalgebra.val_apply Polynomial.aeval_def
isIntegralClosure 📖	mathematical	—	IsIntegralClosure Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring Subalgebra.toAlgebra Algebra.id	—	Subtype.coe_injective

---

← Back to Index