Basic

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

Statistics

Metric	Count
Definitions instMulSemiringActionSubtypeMemSubalgebraIntegralClosure, integralClosure	2
Theorems isIntegral_iff, of_finite, of_injective, of_surjective, prod, tensorProduct, isIntegral_of_surjective, add, mul, neg, neg_iff, of_finite, of_mem_closure, of_mem_of_fg, of_neg, smul, sub, tmul, isIntegral, to_isIntegral, of_finite, add, mul, neg, neg_iff, of_mem_closure, of_neg, sub, isIntegral_iff, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, coe_smul, isIntegral_of_noetherian, isIntegral_of_smul_mem_submodule, isIntegral_of_submodule_noetherian, mem_integralClosure_iff	36
Total	38

AlgEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_iff 📖	mathematical	—	Algebra.IsIntegral	—	Algebra.IsIntegral.of_injective AlgEquivClass.toAlgHomClass instAlgEquivClass injective

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap	IsIntegral	—	IsIntegral.of_surjective IsIntegral.of_finite Module.Finite.self

Algebra.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_finite 📖	mathematical	—	Algebra.IsIntegral	—	IsIntegral.of_finite
of_injective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	Algebra.IsIntegral	—	isIntegral_algHom_iff isIntegral
of_surjective 📖	mathematical	DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring AlgHom.funLike	Algebra.IsIntegral	—	Algebra.isIntegral_def IsIntegral.map IsScalarTower.left AlgHom.algHomClass
prod 📖	mathematical	—	Algebra.IsIntegral Prod.instRing Prod.algebra CommRing.toCommSemiring Ring.toSemiring	—	Algebra.isIntegral_def IsIntegral.pair
tensorProduct 📖	mathematical	—	Algebra.IsIntegral TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule CommSemiring.toSemiring Algebra.TensorProduct.instRing CommRing.toRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass	—	Algebra.to_smulCommClass TensorProduct.induction_on isIntegral_zero IsIntegral.tmul isIntegral IsIntegral.add

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsIntegral CommRing.toRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHom.IsIntegralElem.add
mul 📖	mathematical	IsIntegral CommRing.toRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHom.IsIntegralElem.mul
neg 📖	mathematical	IsIntegral	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	of_mem_of_fg fg_adjoin_singleton Subalgebra.neg_mem Algebra.subset_adjoin
neg_iff 📖	mathematical	—	IsIntegral NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	of_neg neg
of_finite 📖	mathematical	—	IsIntegral	—	smulCommClass_self IsScalarTower.left isIntegral_algHom_iff Algebra.lmul_injective Algebra.IsIntegral.isIntegral Module.End.isIntegral
of_mem_closure 📖	—	IsIntegral CommRing.toRing Subring SetLike.instMembership Subring.instSetLike Subring.closure Set Set.instInsert Set.instSingletonSet	—	—	RingHom.IsIntegralElem.of_mem_closure
of_mem_of_fg 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring Algebra.toModule DFunLike.coe OrderEmbedding Subalgebra Submodule Preorder.toLE PartialOrder.toPreorder Subalgebra.instPartialOrder Submodule.instPartialOrder instFunLikeOrderEmbedding Subalgebra.toSubmodule SetLike.instMembership Subalgebra.instSetLike	IsIntegral	—	Module.Finite.of_fg isIntegral_algHom_iff Subtype.val_injective of_finite
of_neg 📖	—	IsIntegral NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—	neg neg_neg
smul 📖	mathematical	IsIntegral	Algebra.toSMul Ring.toSemiring	—	of_mem_of_fg fg_adjoin_singleton algebraMap_smul Subalgebra.smul_mem Algebra.subset_adjoin
sub 📖	mathematical	IsIntegral CommRing.toRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	RingHom.IsIntegralElem.sub
tmul 📖	mathematical	IsIntegral	TensorProduct CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule CommSemiring.toSemiring Ring.toSemiring Algebra.TensorProduct.instRing CommRing.toRing Algebra.TensorProduct.leftAlgebra Algebra.id Algebra.to_smulCommClass TensorProduct.tmul	—	Algebra.to_smulCommClass mul_one smul_eq_mul TensorProduct.smul_tmul' smul TensorProduct.isScalarTower_left IsScalarTower.right map_of_comp_eq Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral 📖	mathematical	—	Algebra.IsIntegral Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instRing instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	smulCommClass_self IsScalarTower.left LinearMap.exists_monic_and_aeval_eq_zero

RingHom.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_isIntegral 📖	mathematical	—	RingHom.IsIntegral CommRing.toRing	—	IsIntegral.of_mem_of_fg Module.Finite.fg_top

RingHom.IsIntegral

Theorems

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

RingHom.IsIntegralElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	RingHom.IsIntegralElem CommRing.toRing	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	of_mem_closure Subring.add_mem Subring.subset_closure
mul 📖	mathematical	RingHom.IsIntegralElem CommRing.toRing	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	of_mem_closure Subring.mul_mem Subring.subset_closure
neg 📖	mathematical	RingHom.IsIntegralElem CommRing.toRing	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	of_mem_closure Subring.neg_mem Subring.subset_closure
neg_iff 📖	mathematical	—	RingHom.IsIntegralElem CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	of_neg neg
of_mem_closure 📖	—	RingHom.IsIntegralElem CommRing.toRing Subring SetLike.instMembership Subring.instSetLike Subring.closure Set Set.instInsert Set.instSingletonSet	—	—	IsScalarTower.right Submodule.FG.mul IsIntegral.fg_adjoin_singleton IsIntegral.of_mem_of_fg Set.singleton_union Algebra.adjoin_union_coe_submodule Algebra.mem_adjoin_iff Subring.closure_mono Set.subset_union_right
of_neg 📖	—	RingHom.IsIntegralElem CommRing.toRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	—	neg neg_neg
sub 📖	mathematical	RingHom.IsIntegralElem CommRing.toRing	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	sub_eq_add_neg add neg

Subalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIntegral_iff 📖	mathematical	—	Algebra.IsIntegral Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership instSetLike toRing algebra IsIntegral	—	Algebra.isIntegral_def isIntegral_algHom_iff Subtype.val_injective

(root)

Definitions

Name	Category	Theorems
instMulSemiringActionSubtypeMemSubalgebraIntegralClosure 📖	CompOp	3 math math: instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, integralClosure.coe_smul, instSMulCommClassSubtypeMemSubalgebraIntegralClosure
integralClosure 📖	CompOp	73 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, integralClosure_le_span_dualBasis, ValuationSubring.integralClosure_algebraMap_injective, integralClosure_le_completeIntegralClosure, TensorProduct.toIntegralClosure_bijective_of_isLocalization, integralClosure.AlgebraIsIntegral, AlgHom.coe_mapIntegralClosure, adjoin_le_integralClosure, integralClosure.isIntegrallyClosedOfFiniteExtension, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, integralClosure_map_algEquiv, instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure, integralClosure_eq_top_iff, TensorProduct.toIntegralClosure_bijective_of_smooth, AlgebraicGeometry.Scheme.Hom.toNormalization_app_preimage, IsIntegrallyClosedIn.integralClosure_eq_bot, integralClosure_idem, Subring.integralClosure_subring_le_iff, integralClosure.isDedekindDomain, instSMulDistribClassSubtypeMemSubalgebraIntegralClosure, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, mem_adjoin_map_integralClosure_of_isStandardEtale, completeIntegralClosure_eq_integralClosure, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, iInf_valuationSubring_superset, integralClosure.isFractionRing_of_finite_extension, TensorProduct.toIntegralClosure_mvPolynomial_bijective, integralClosure_le_algebraicClosure, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, roots_mem_integralClosure, NumberField.house.exists_ne_zero_int_vec_house_le, mem_integralClosure_iff_mem_fg, Subalgebra.algebraicClosure_eq_integralClosure, AlgEquiv.coe_mapIntegralClosure, le_integralClosure_iff_isIntegral, integralClosure.isNoetherianRing, Algebra.zariskisMainProperty_iff_exists_saturation_eq_top, IsIntegrallyClosed.integralClosure_eq_bot, IsIntegrallyClosed.integralClosure_eq_bot_iff, NumberField.RingOfIntegers.mk_zero, Ideal.IntegralClosure.isMaximal_of_isMaximal_comap, instIsIntegrallyClosedInSubtypeMemSubalgebraIntegralClosure, mem_integralClosure_iff, IsIntegrallyClosedIn.integralClosure_eq_bot_iff, ValuationSubring.isIntegral_of_mem_ringOfIntegers', integralClosure.isFractionRing_of_algebraic, Ring.DimensionLEOne.integralClosure, algebraicClosure_toSubalgebra, NumberField.RingOfIntegers.mk_one, Subring.integralClosure_le_iff, minpoly.ofSubring, AlgebraicGeometry.Scheme.Hom.ι_toNormalization_assoc, AlgebraicGeometry.Scheme.Hom.fromNormalization_app_assoc, integralClosure.coe_smul, TensorProduct.toIntegralClosure_injective_of_flat, AlgebraicIndependent.integralClosure, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, Valuation.Integers.integralClosure, IsLocalization.integralClosure, IsPrimitiveRoot.coe_toInteger, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, integralClosure.isDedekindDomain_fractionRing, Algebra.exists_etale_isIdempotentElem_forall_liesOver_eq_aux, instSMulCommClassSubtypeMemSubalgebraIntegralClosure, instIsDomainSubtypeMemSubalgebraIntegralClosure, integralClosure.isIntegral, integralClosure.isIntegralClosure, AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val, Algebra.exists_notMem_and_isIntegral_forall_mem_of_ne_of_liesOver, IsLocalization.Away.integralClosure, integralClosure.mem_lifts_of_monic_of_dvd_map, AlgebraicGeometry.Scheme.Hom.fromNormalization_app, Transcendental.integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSMulCommClassSubtypeMemSubalgebraIntegralClosure 📖	mathematical	—	SMulCommClass Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subalgebra.toRing CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Subalgebra.toSemiring instMulSemiringActionSubtypeMemSubalgebraIntegralClosure Algebra.toSMul Subalgebra.algebra	—	SMulCommClass.smul_comm
instSMulDistribClassSubtypeMemSubalgebraIntegralClosure 📖	mathematical	—	SMulDistribClass Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subalgebra.toRing CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Subalgebra.toSemiring instMulSemiringActionSubtypeMemSubalgebraIntegralClosure Ring.toSemiring Subalgebra.instSMulSubtypeMem Algebra.toSMul Algebra.id	—	smul_mul'
isIntegral_of_noetherian 📖	mathematical	—	IsIntegral	—	IsIntegral.of_finite Module.IsNoetherian.finite
isIntegral_of_smul_mem_submodule 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule SetLike.instMembership Submodule.setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	IsIntegral CommRing.toRing	—	smul_smul one_smul Submodule.add_mem add_smul Submodule.zero_mem zero_smul Submodule.smul_mem algebraMap_smul smulCommClass_self Submodule.isScalarTower' IsScalarTower.left Subalgebra.smulCommClass_left IsScalarTower.to_smulCommClass' Subtype.prop LinearMap.ext smul_assoc SemigroupAction.mul_smul eq_bot_iff Mathlib.Tactic.Push.not_and_eq LinearMap.ker_eq_bot LinearMap.congr_fun smul_eq_zero_iff_left IsDomain.toIsCancelMulZero isIntegral_algHom_iff Subtype.val_injective Algebra.IsIntegral.isIntegral Module.End.isIntegral Module.Finite.iff_fg
isIntegral_of_submodule_noetherian 📖	mathematical	Subalgebra CommRing.toCommSemiring Ring.toSemiring SetLike.instMembership Subalgebra.instSetLike	IsIntegral	—	IsIntegral.of_mem_of_fg Submodule.fg_top IsNoetherian.noetherian
mem_integralClosure_iff 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure IsIntegral CommRing.toRing	—	—

integralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_smul 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subalgebra.toRing CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid MulSemiringAction.toDistribMulAction Subalgebra.toSemiring instMulSemiringActionSubtypeMemSubalgebraIntegralClosure Ring.toSemiring	—	—

---

← Back to Index