Integral

📁 Source: Mathlib/RingTheory/Localization/Integral.lean

Statistics

Metric	Count
Definitions coeffIntegerNormalization, integerNormalization	2
Theorems comap_isAlgebraic_iff, ideal_span_singleton_map_subset, integerNormalization_eq_zero_iff, isAlgebraic_iff, isAlgebraic_iff', exists_multiple_integral_of_isLocalization, isFractionRing_of_algebraic, isFractionRing_of_finite_extension, exists_isIntegral_mul_of_isIntegral_algebraMap, exists_isIntegral_mul_of_isIntegral_mk', integralClosure, isIntegral_of_isIntegral_map, coeffIntegerNormalization_mem_support, coeffIntegerNormalization_of_coeff_zero, exists_isIntegral_smul_of_isIntegral_map, integerNormalization_aeval_eq_zero, integerNormalization_coeff, integerNormalization_eval₂_eq_zero, integerNormalization_map_to_map, integerNormalization_spec, integralClosure, scaleRoots_commonDenom_mem_lifts, isIntegralElem_localization_at_leadingCoeff, isFractionRing_of_algebraic, isFractionRing_of_finite_extension, isAlgebraic_of_isFractionRing, isIntegral_localization, isIntegral_localization', isIntegral_of_isIntegral_adjoin_of_mul_eq_one, is_integral_localization_at_leadingCoeff	30
Total	32

IsFractionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_isAlgebraic_iff 📖	mathematical	—	Algebra.IsAlgebraic CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	isAlgebraic_iff Algebra.IsAlgebraic.isAlgebraic
ideal_span_singleton_map_subset 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Set Set.instHasSubset SetLike.coe Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Ideal.span Set.instSingletonSet Submodule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule Submodule.span	EuclideanDomain.toCommRing Field.toEuclideanDomain Semifield.toCommSemiring Set.image	—	Ideal.mem_span_singleton IsLocalization.exists_mk'_eq Algebra.IsAlgebraic.exists_smul_eq_mul IsDomain.to_noZeroDivisors nonZeroDivisors.coe_ne_zero IsDomain.toNontrivial Function.Injective.of_comp RingHom.coe_comp IsScalarTower.algebraMap_eq map_mem_nonZeroDivisors MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mem_nonZeroDivisors_of_ne_zero IsLocalization.mk'_eq_of_eq mul_comm Algebra.smul_def Submodule.span_subset_span RingHomSurjective.ids LinearMap.IsScalarTower.compatibleSMul' Submodule.span_algebraMap_image_of_tower Submodule.mem_map_of_mem mk'_eq_div IsScalarTower.algebraMap_apply div_eq_mul_inv mul_assoc map_inv₀ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Submodule.smul_mem
integerNormalization_eq_zero_iff 📖	mathematical	—	IsLocalization.integerNormalization nonZeroDivisors Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial Polynomial.instZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Polynomial.ext_iff IsLocalization.integerNormalization_spec Polynomial.coeff_zero to_map_eq_zero_iff smul_zero NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain Algebra.smul_def mem_nonZeroDivisors_iff_ne_zero IsDomain.toNontrivial
isAlgebraic_iff 📖	mathematical	—	IsAlgebraic CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Polynomial.ext trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv Polynomial.coeff_map to_map_eq_zero_iff Polynomial.aeval_map_algebraMap integerNormalization_eq_zero_iff IsLocalization.integerNormalization_aeval_eq_zero
isAlgebraic_iff' 📖	mathematical	—	Algebra.IsAlgebraic CommRing.toRing DivisionRing.toRing Field.toDivisionRing	—	IsScalarTower.right Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero EuclideanDomain.toNontrivial FractionRing.isScalarTower_liftAlgebra isAlgebraic_iff Localization.isLocalization isAlgebraic_iff_isIntegral div_surjective div_eq_mul_inv IsIntegral.mul IsAlgebraic.extendScalars FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial IsAlgebraic.algebraMap IsIntegral.inv injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass instFaithfulSMul Polynomial.aeval_algebraMap_apply

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_multiple_integral_of_isLocalization 📖	mathematical	IsIntegral CommRing.toRing	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike Submonoid.smul Algebra.toSMul	—	subsingleton_or_nontrivial Polynomial.monic_X RingHom.codomain_trivial Polynomial.lifts_and_natDegree_eq_and_monic IsLocalization.scaleRoots_commonDenom_mem_lifts Polynomial.Monic.leadingCoeff OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass SubringClass.toSubsemiringClass Subring.instSubringClass Polynomial.monic_scaleRoots_iff IsScalarTower.algebraMap_eq Polynomial.eval₂_map Submonoid.smul_def Algebra.smul_def IsScalarTower.algebraMap_apply Polynomial.scaleRoots_eval₂_eq_zero

IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFractionRing_of_algebraic 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsFractionRing CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield	—	mem_nonZeroDivisors_iff_ne_zero IsDomain.to_noZeroDivisors IsDomain.toNontrivial injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass algebraMap_injective IsAlgebraic.exists_integral_multiple Algebra.IsAlgebraic.isAlgebraic mem_nonZeroDivisors_of_ne_zero IsScalarTower.algebraMap_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass algebraMap_mk' Algebra.smul_def mul_comm one_mul
isFractionRing_of_finite_extension 📖	mathematical	—	IsFractionRing CommRing.toCommSemiring Semifield.toCommSemiring Field.toSemifield	—	IsFractionRing.comap_isAlgebraic_iff Algebra.IsAlgebraic.of_finite EuclideanDomain.toNontrivial isFractionRing_of_algebraic IsFractionRing.to_map_eq_zero_iff map_eq_zero RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsScalarTower.algebraMap_apply

IsLocalization

Definitions

Name	Category	Theorems
coeffIntegerNormalization 📖	CompOp	2 math math: coeffIntegerNormalization_of_coeff_zero, integerNormalization_coeff
integerNormalization 📖	CompOp	6 math math: integerNormalization_map_to_map, IsFractionRing.integerNormalization_eq_zero_iff, integerNormalization_coeff, integerNormalization_aeval_eq_zero, integerNormalization_eval₂_eq_zero, integerNormalization_spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeffIntegerNormalization_mem_support 📖	mathematical	—	Finset Finset.instMembership Polynomial.support CommSemiring.toSemiring CommRing.toCommSemiring	—	Mathlib.Tactic.Contrapose.contrapose₂ coeffIntegerNormalization.eq_1
coeffIntegerNormalization_of_coeff_zero 📖	mathematical	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	coeffIntegerNormalization	—	—
exists_isIntegral_smul_of_isIntegral_map 📖	mathematical	IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Algebra.toSMul	—	IsScalarTower.algebraMap_eq map_eq_zero_iff Algebra.smul_def Polynomial.leadingCoeff_mul_monic Polynomial.leadingCoeff_C RingHom.isIntegralElem_leadingCoeff_mul Polynomial.eval₂_mul Polynomial.eval₂_C
integerNormalization_aeval_eq_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	integerNormalization	—	Polynomial.aeval_def IsScalarTower.algebraMap_eq integerNormalization_eval₂_eq_zero
integerNormalization_coeff 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring integerNormalization coeffIntegerNormalization	—	Polynomial.finset_sum_coeff Finset.sum_congr Polynomial.coeff_monomial coeffIntegerNormalization.congr_simp Finset.sum_ite_eq' coeffIntegerNormalization_of_coeff_zero
integerNormalization_eval₂_eq_zero 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	RingHom.comp Semiring.toNonAssocSemiring algebraMap integerNormalization	—	integerNormalization_map_to_map trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv Polynomial.eval₂_map IsScalarTower.algebraMap_smul Polynomial.isScalarTower IsScalarTower.right Polynomial.eval₂_smul MulZeroClass.mul_zero
integerNormalization_map_to_map 📖	mathematical	—	Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring algebraMap integerNormalization Polynomial Algebra.toSMul Polynomial.semiring Polynomial.algebraOfAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	—	integerNormalization_spec Polynomial.ext Polynomial.coeff_map Polynomial.coeff_smul
integerNormalization_spec 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Polynomial.coeff integerNormalization Algebra.toSMul Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike	—	exist_integer_multiples_of_finset integerNormalization_coeff coeffIntegerNormalization.eq_1 Finset.mem_image map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.notMem_support_iff smul_zero
integralClosure 📖	mathematical	—	IsLocalization Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring Algebra.algebraMapSubmonoid Subalgebra.toSemiring Subalgebra.algebra	—	Subalgebra.instIsScalarTowerSubtypeMem IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_units surj IsIntegral.exists_multiple_integral_of_isLocalization exists_isIntegral_smul_of_isIntegral_map Algebra.smul_def map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass IsIntegral.mul IsIntegral.algebraMap IsScalarTower.left Algebra.IsIntegral.isIntegral Algebra.IsIntegral.of_finite Module.Finite.self MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass FaithfulSMul.algebraMap_injective Subalgebra.instFaithfulSMulSubtypeMem instFaithfulSMul SubsemiringClass.toSubmonoidClass Subalgebra.instSubsemiringClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul eq_iff_exists
scaleRoots_commonDenom_mem_lifts 📖	mathematical	Subring CommRing.toRing SetLike.instMembership Subring.instSetLike RingHom.range algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Polynomial.leadingCoeff	Polynomial Subsemiring Semiring.toNonAssocSemiring Polynomial.semiring Subsemiring.instSetLike Polynomial.lifts Polynomial.scaleRoots DFunLike.coe RingHom RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike commonDenom Polynomial.support Polynomial.coeff	—	Polynomial.lifts_iff_coeff_lifts Polynomial.coeff_scaleRoots Polynomial.coeff_natDegree tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one lt_of_le_of_ne Polynomial.le_natDegree_of_mem_supp tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid le_tsub_of_add_le_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le pow_add pow_one mul_comm mul_assoc map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass SubringClass.toSubsemiringClass Subring.instSubringClass RingHom.mem_range_self Algebra.smul_def map_integerMultiple Polynomial.notMem_support_iff MulZeroClass.zero_mul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass

IsLocalization.Away

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isIntegral_mul_of_isIntegral_algebraMap 📖	mathematical	IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton IsScalarTower.algebraMap_eq IsLocalization.map_eq_zero_iff isIntegral_trans IsScalarTower.subalgebra' IsScalarTower.right integralClosure.AlgebraIsIntegral isIntegral_leadingCoeff_smul map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_C Polynomial.aeval_map_algebraMap Polynomial.Monic.leadingCoeff_C_mul Polynomial.Monic.map RingHom.instRingHomClass
exists_isIntegral_mul_of_isIntegral_mk' 📖	mathematical	IsIntegral CommRing.toRing IsLocalization.mk' CommRing.toCommSemiring Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow	—	exists_isIntegral_mul_of_isIntegral_algebraMap IsIntegral.mul IsIntegral.algebraMap IsIntegral.pow
integralClosure 📖	mathematical	—	IsLocalization.Away Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Subalgebra.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebra	—	Algebra.algebraMapSubmonoid_powers IsLocalization.integralClosure instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap
isIntegral_of_isIntegral_map 📖	—	IsIntegral CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	—	IsScalarTower.algebraMap_eq IsLocalization.map_eq_zero_iff Polynomial.Monic.mul Polynomial.monic_X_pow Polynomial.eval₂_mul Polynomial.eval₂_X_pow

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegralElem_localization_at_leadingCoeff 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike Polynomial.leadingCoeff	IsIntegralElem CommRing.toRing IsLocalization.map CommRing.toCommSemiring Submonoid.map RingHom instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass Submonoid.le_comap_map DFunLike.coe algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass Submonoid.le_comap_map trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv Polynomial.leadingCoeff_zero Polynomial.eval₂_zero isUnit_iff_exists_inv instIsDedekindFiniteMonoid IsLocalization.map_units Polynomial.monic_mul_C_of_leadingCoeff_mul_eq_one Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero zero_ne_one NeZero.one nontrivial_of_ne MulZeroClass.zero_mul Polynomial.eval₂_mul_eq_zero_of_left Polynomial.eval₂_map IsLocalization.map_comp Polynomial.hom_eval₂ map_zero MonoidWithZeroHomClass.toZeroHomClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isAlgebraic_of_isFractionRing 📖	mathematical	—	Algebra.IsAlgebraic EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing	—	IsLocalization.exists_mk'_eq IsIntegral.isAlgebraic EuclideanDomain.toNontrivial IsLocalization.mk'_eq_mul_mk'_one RingHom.IsIntegralElem.mul IsIntegral.tower_top IsIntegral.map IsScalarTower.left AlgHom.algHomClass Algebra.IsIntegral.isIntegral isAlgebraic_iff_isIntegral IsAlgebraic.invOf_iff
isIntegral_localization 📖	mathematical	—	RingHom.IsIntegral CommRing.toRing IsLocalization.map CommRing.toCommSemiring Algebra.algebraMapSubmonoid CommSemiring.toSemiring algebraMap	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Submonoid.le_comap_map IsLocalization.surj isUnit_iff_exists_inv' instIsDedekindFiniteMonoid IsLocalization.map_units IsIntegral.of_mul_unit IsLocalization.map_eq localizationAlgebraMap_def map_one MonoidHomClass.toOneHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Algebra.IsIntegral.isIntegral is_integral_localization_at_leadingCoeff Submonoid.one_mem
isIntegral_localization' 📖	mathematical	RingHom.IsIntegral CommRing.toRing	Localization CommRing.toCommMonoid Submonoid.map MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toMulOneClass CommMonoid.toMonoid MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike MonoidHom.instMonoidHomClass MonoidHomClass.toMonoidHom RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass OreLocalization.instCommRing OreLocalization.oreSetComm OreLocalization.instRing IsLocalization.map OreLocalization.instCommSemiring OreLocalization.instAlgebra Algebra.id Localization.isLocalization Ring.toSemiring Submonoid.le_comap_map	—	MonoidHom.instMonoidHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Localization.isLocalization isIntegral_localization
isIntegral_of_isIntegral_adjoin_of_mul_eq_one 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing IsIntegral Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet Polynomial.instCommRingAdjoinSingleton Subalgebra.toAlgebra Ring.toSemiring Algebra.id	—	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton Polynomial.lifts_iff_coeff_lifts Polynomial.coeff_map Polynomial.lifts_and_degree_eq_and_monic Polynomial.Monic.map Polynomial.eval_map Finset.le_sup Nat.instCanonicallyOrderedAdd Polynomial.aeval_def mul_comm Polynomial.eval₂_reflect_mul_pow LE.le.trans Polynomial.natDegree_reflect_le sup_of_le_left Polynomial.reflect_reflect Polynomial.monic_of_natDegree_le_of_coeff_eq_one Polynomial.natDegree_sum_le_of_forall_le le_imp_le_of_le_of_le Polynomial.natDegree_mul_le le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.natDegree_pow_le mul_le_mul_right Nat.instMulLeftMono Polynomial.natDegree_X_le add_le_add_right mul_one max_eq_left IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Polynomial.le_natDegree_of_mem_supp Polynomial.finset_sum_coeff Finset.sum_congr Polynomial.coeff_X_pow_mul' Polynomial.coeff_reflect Finset.sum_eq_single add_lt_add_left IsRightCancelAdd.addRightStrictMono_of_addRightMono LE.le.lt_of_ne add_comm IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instOrderedSub LT.lt.not_ge Polynomial.coeff_eq_zero_of_natDegree_lt zero_add tsub_zero Polynomial.revAt_le tsub_self Polynomial.Monic.leadingCoeff add_tsub_cancel_left Polynomial.coeff_one_zero map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X mul_left_comm MulZeroClass.zero_mul
is_integral_localization_at_leadingCoeff 📖	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 Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike Polynomial.leadingCoeff	RingHom.IsIntegralElem CommRing.toRing IsLocalization.map Algebra.algebraMapSubmonoid algebraMap RingHom RingHom.instFunLike	—	RingHom.isIntegralElem_localization_at_leadingCoeff

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFractionRing_of_algebraic 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	IsFractionRing Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring Semifield.toCommSemiring Field.toSemifield Subalgebra.toAlgebra Algebra.id	—	IsIntegralClosure.isFractionRing_of_algebraic instIsDomainSubtypeMemSubalgebraIntegralClosure instIsDomain isIntegralClosure IsScalarTower.subalgebra' IsScalarTower.right
isFractionRing_of_finite_extension 📖	mathematical	—	IsFractionRing Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toCommSemiring Semifield.toCommSemiring Field.toSemifield Subalgebra.toAlgebra Algebra.id	—	IsIntegralClosure.isFractionRing_of_finite_extension instIsDomainSubtypeMemSubalgebraIntegralClosure instIsDomain isIntegralClosure IsScalarTower.subalgebra' IsScalarTower.right

---

← Back to Index