GoingUp

📁 Source: Mathlib/RingTheory/Ideal/GoingUp.lean

Statistics

Metric	Count
Definitions	0
Theorems comap_lt_comap, comap_ne_bot, eq_bot_of_comap_eq_bot, isMaximal_of_isMaximal_comap, comap_lt_comap, comap_ne_bot, eq_bot_of_comap_eq_bot, isMaximal_of_isMaximal_comap, of_isMaximal_liesOver, of_liesOver_isMaximal, under, algebra_isIntegral_of_liesOver, coeff_zero_mem_comap_of_root_mem, coeff_zero_mem_comap_of_root_mem_of_eval_mem, comap_lt_comap_of_integral_mem_sdiff, comap_lt_comap_of_root_mem_sdiff, comap_ne_bot_of_algebraic_mem, comap_ne_bot_of_integral_mem, comap_ne_bot_of_root_mem, eq_bot_of_comap_eq_bot, eq_bot_of_liesOver_bot, exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff, exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem, exists_coeff_ne_zero_mem_comap_of_root_mem, exists_ideal_liesOver_maximal_of_isIntegral, exists_ideal_over_maximal_of_isIntegral, exists_ideal_over_prime_of_isIntegral, exists_ideal_over_prime_of_isIntegral_of_isDomain, exists_ideal_over_prime_of_isIntegral_of_isPrime, exists_maximal_ideal_liesOver_of_isIntegral, exists_nonzero_mem_of_ne_bot, exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton, injective_quotient_le_comap_map, isMaximal_comap_of_isIntegral_of_isMaximal, isMaximal_comap_of_isIntegral_of_isMaximal', isMaximal_of_isIntegral_of_isMaximal_comap, isMaximal_of_isIntegral_of_isMaximal_comap', isMaximal_of_mem_primesOver, map_eq_top_iff, map_eq_top_iff_of_ker_le, mem_of_one_mem, nonempty_primesOver, isMaximal, primesOver_bot, quotient_mk_maps_eq, under_ne_bot	46
Total	46

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_zero_mem_comap_of_root_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	comap RingHom RingHom.instFunLike RingHom.instRingHomClass Polynomial.coeff	—	coeff_zero_mem_comap_of_root_mem_of_eval_mem zero_mem
coeff_zero_mem_comap_of_root_mem_of_eval_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.eval₂	comap RingHom RingHom.instFunLike RingHom.instRingHomClass Polynomial.coeff	—	RingHom.instRingHomClass mem_comap add_mem_iff_right mul_mem_left Polynomial.eval₂_X Polynomial.eval₂_mul Polynomial.eval₂_C Polynomial.eval₂_add Polynomial.divX_mul_X_add
comap_lt_comap_of_integral_mem_sdiff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instMembership Set.instSDiff SetLike.coe Submodule.setLike IsIntegral CommRing.toRing	Preorder.toLT comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	RingHom.instRingHomClass comap_lt_comap_of_root_mem_sdiff Polynomial.map_monic_ne_zero instIsTwoSided_1 IsDomain.toNontrivial Quotient.isDomain IsPrime.under zero_mem
comap_lt_comap_of_root_mem_sdiff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instMembership Set.instSDiff SetLike.coe Submodule.setLike SetLike.instMembership Polynomial.eval₂	Preorder.toLT comap RingHom RingHom.instFunLike RingHom.instRingHomClass	—	RingHom.instRingHomClass instIsTwoSided_1 exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff SetLike.lt_iff_le_and_exists instIsConcreteLE comap_mono
comap_ne_bot_of_algebraic_mem 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsAlgebraic CommRing.toRing	—	—	RingHom.instRingHomClass comap_ne_bot_of_root_mem
comap_ne_bot_of_integral_mem 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsIntegral CommRing.toRing	—	—	comap_ne_bot_of_algebraic_mem IsIntegral.isAlgebraic
comap_ne_bot_of_root_mem 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—	RingHom.instRingHomClass exists_coeff_ne_zero_mem_comap_of_root_mem mem_bot eq_bot_iff
eq_bot_of_comap_eq_bot 📖	—	comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—	RingHom.instRingHomClass eq_bot_iff zero_mem comap_ne_bot_of_integral_mem Algebra.IsIntegral.isIntegral
eq_bot_of_liesOver_bot 📖	mathematical	—	Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	eq_bot_of_comap_eq_bot liesOver_iff
exists_coeff_mem_comap_sdiff_comap_of_root_mem_sdiff 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instMembership Set.instSDiff SetLike.coe Submodule.setLike SetLike.instMembership Polynomial.eval₂	comap RingHom RingHom.instFunLike RingHom.instRingHomClass Polynomial.coeff	—	RingHom.instRingHomClass instIsTwoSided_1 Submodule.Quotient.mk_eq_zero mem_map_of_mem trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv Polynomial.eval₂_map Polynomial.hom_eval₂ Quotient.eq_zero_iff_mem exists_coeff_ne_zero_mem_comap_of_root_mem Quotient.isDomain mem_quotient_iff_mem Polynomial.coeff_map
exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.eval₂	comap RingHom RingHom.instFunLike RingHom.instRingHomClass Polynomial.coeff	—	RingHom.instRingHomClass Polynomial.coeff_add Polynomial.coeff_C_zero zero_add coeff_zero_mem_comap_of_root_mem Polynomial.eval₂_X Polynomial.eval₂_mul Polynomial.coeff_mul_X
exists_coeff_ne_zero_mem_comap_of_root_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Polynomial.eval₂ MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	comap RingHom RingHom.instFunLike RingHom.instRingHomClass Polynomial.coeff	—	exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem mul_eq_zero IsDomain.to_noZeroDivisors
exists_ideal_liesOver_maximal_of_isIntegral 📖	mathematical	—	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring LiesOver	—	exists_maximal_ideal_liesOver_of_isIntegral
exists_ideal_over_maximal_of_isIntegral 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap	IsMaximal comap	—	RingHom.instRingHomClass exists_ideal_over_prime_of_isIntegral IsMaximal.isPrime' isMaximal_of_isIntegral_of_isMaximal_comap
exists_ideal_over_prime_of_isIntegral 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	IsPrime	—	RingHom.instRingHomClass exists_ideal_comap_le_prime exists_ideal_over_prime_of_isIntegral_of_isPrime LE.le.trans
exists_ideal_over_prime_of_isIntegral_of_isDomain 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass algebraMap	IsPrime comap	—	RingHom.instRingHomClass exists_maximal IsDomain.toNontrivial IsLocalization.isDomain_localization le_nonZeroDivisors_of_noZeroDivisors IsDomain.to_noZeroDivisors Localization.isLocalization isIntegral_localization isMaximal_comap_of_isIntegral_of_isMaximal comap_isPrime IsMaximal.isPrime' Localization.AtPrime.isLocalRing comap_comap IsLocalRing.eq_maximalIdeal Algebra.mem_algebraMapSubmonoid_of_mem IsLocalization.map_comp Localization.AtPrime.comap_maximalIdeal
exists_ideal_over_prime_of_isIntegral_of_isPrime 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	IsPrime	—	RingHom.instRingHomClass instIsTwoSided_1 exists_ideal_over_prime_of_isIntegral_of_isDomain Quotient.isDomain Algebra.IsIntegral.quotient map_isPrime_of_surjective Quotient.mk_surjective mk_ker le_trans le_of_eq RingHom.injective_iff_ker_eq_bot algebraMap_quotient_injective bot_le ker_le_comap comap_isPrime comap_comap trans IsPreorder.toIsTrans IsEquiv.toIsPreorder eq_isEquiv RingHom.ext comap_map_of_surjective sup_eq_left
exists_maximal_ideal_liesOver_of_isIntegral 📖	mathematical	—	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring LiesOver	—	exists_ideal_over_maximal_of_isIntegral RingHom.instRingHomClass RingHom.injective_iff_ker_eq_bot FaithfulSMul.algebraMap_injective
exists_nonzero_mem_of_ne_bot 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ideal Polynomial.semiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	RingHom.instRingHomClass instIsTwoSided_1 Submodule.nonzero_mem_of_bot_lt bot_lt_iff_ne_bot Submodule.coe_mem Submodule.coe_eq_zero injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass Polynomial.map_injective RingHom.injective_iff_ker_eq_bot mk_ker Submodule.eq_bot_iff mem_comap
exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton 📖	mathematical	primesOver CommRing.toCommSemiring CommSemiring.toSemiring Ideal Set Set.instSingletonSet SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	mul_comm exists_le_prime_disjoint Mathlib.Tactic.Push.not_and_eq Set.subset_compl_iff_disjoint_right RingHom.instRingHomClass exists_ideal_over_prime_of_isIntegral_of_isPrime mem_span_singleton_self Eq.le
injective_quotient_le_comap_map 📖	mathematical	—	HasQuotient.Quotient Polynomial Ring.toSemiring CommRing.toRing Ideal Polynomial.ring instHasQuotient comap CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RingHom.instRingHomClass Quotient.ring instIsTwoSided_1 Quotient.instRingQuotient map Polynomial.mapRingHom DFunLike.coe Polynomial.commRing Quotient.commRing quotientMap le_comap_map	—	quotientMap_injective' RingHom.instRingHomClass instIsTwoSided_1 le_comap_map le_of_eq comap_map_of_surjective Polynomial.map_surjective Quotient.mk_surjective le_antisymm sup_le le_rfl polynomial_mem_ideal_of_coeff_mem_ideal Quotient.eq_zero_iff_mem Polynomial.coeff_map Polynomial.ext_iff mem_bot mem_comap le_sup_of_le_left
isMaximal_comap_of_isIntegral_of_isMaximal 📖	mathematical	—	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	Quotient.maximal_of_isField RingHom.instRingHomClass isField_of_isIntegral_of_isField instIsTwoSided_1 Algebra.IsIntegral.quotient algebraMap_quotient_injective Quotient.maximal_ideal_iff_isField_quotient
isMaximal_comap_of_isIntegral_of_isMaximal' 📖	mathematical	RingHom.IsIntegral CommRing.toRing	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike RingHom.instRingHomClass	—	isMaximal_comap_of_isIntegral_of_isMaximal
isMaximal_of_isIntegral_of_isMaximal_comap 📖	mathematical	—	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHom.instRingHomClass comap_eq_top_iff IsMaximal.out SetLike.lt_iff_le_and_exists instIsConcreteLE comap_lt_comap_of_integral_mem_sdiff Algebra.IsIntegral.isIntegral
isMaximal_of_isIntegral_of_isMaximal_comap' 📖	mathematical	RingHom.IsIntegral CommRing.toRing	IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHom.instRingHomClass isMaximal_of_isIntegral_of_isMaximal_comap
isMaximal_of_mem_primesOver 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership primesOver	IsMaximal	—	primesOver.isMaximal
map_eq_top_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.IsIntegral CommRing.toRing	map Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	map_eq_top_iff_of_ker_le RingHom.instRingHomClass RingHom.injective_iff_ker_eq_bot
map_eq_top_iff_of_ker_le 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.ker RingHom RingHom.instFunLike RingHom.instRingHomClass RingHom.IsIntegral CommRing.toRing	map Top.top Submodule.instTop	—	RingHom.instRingHomClass Mathlib.Tactic.Contrapose.contrapose₁ exists_le_maximal exists_ideal_over_maximal_of_isIntegral LE.le.trans LT.lt.ne LE.le.trans_lt map_le_iff_le_comap lt_top_iff_ne_top IsMaximal.ne_top map_top
mem_of_one_mem 📖	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—	Submodule.mem_top eq_top_iff_one
nonempty_primesOver 📖	mathematical	—	Set.Elem Ideal CommSemiring.toSemiring CommRing.toCommSemiring primesOver	—	RingHom.instRingHomClass exists_ideal_over_prime_of_isIntegral under_bot liesOver_iff
primesOver_bot 📖	mathematical	—	primesOver CommRing.toCommSemiring Bot.bot Ideal CommSemiring.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instSingletonSet	—	Set.ext eq_bot_of_comap_eq_bot IsDomain.toNontrivial isPrime_bot IsDomain.to_noZeroDivisors bot_liesOver_bot
quotient_mk_maps_eq 📖	mathematical	—	RingHom.comp HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient comap Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RingHom.instRingHomClass Quotient.ring instIsTwoSided_1 Polynomial.ring Quotient.instRingQuotient map Polynomial.mapRingHom Polynomial.commRing Quotient.commRing quotientMap le_comap_map	—	RingHom.ext RingHom.instRingHomClass instIsTwoSided_1 le_comap_map Polynomial.map_C
under_ne_bot 📖	—	—	—	—	eq_bot_of_comap_eq_bot

Ideal.IntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_lt_comap 📖	mathematical	Ideal Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal.comap RingHom RingHom.instFunLike algebraMap Subalgebra.algebra RingHom.instRingHomClass	—	Ideal.IsIntegralClosure.comap_lt_comap IsScalarTower.subalgebra' IsScalarTower.right integralClosure.isIntegralClosure
comap_ne_bot 📖	—	—	—	—	Ideal.IsIntegralClosure.comap_ne_bot IsScalarTower.subalgebra' IsScalarTower.right integralClosure.isIntegralClosure instIsDomainSubtypeMemSubalgebraIntegralClosure
eq_bot_of_comap_eq_bot 📖	—	Ideal.comap Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure RingHom Semiring.toNonAssocSemiring Subalgebra.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebra RingHom.instRingHomClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—	Ideal.IsIntegralClosure.eq_bot_of_comap_eq_bot IsScalarTower.subalgebra' IsScalarTower.right integralClosure.isIntegralClosure instIsDomainSubtypeMemSubalgebraIntegralClosure
isMaximal_of_isMaximal_comap 📖	mathematical	—	Ideal.IsMaximal Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toSemiring	—	RingHom.instRingHomClass Ideal.IsIntegralClosure.isMaximal_of_isMaximal_comap IsScalarTower.subalgebra' IsScalarTower.right integralClosure.isIntegralClosure

Ideal.IsIntegralClosure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap_lt_comap 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	Ideal.comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	RingHom.instRingHomClass SetLike.lt_iff_le_and_exists instIsConcreteLE Ideal.comap_lt_comap_of_integral_mem_sdiff IsIntegralClosure.isIntegral
comap_ne_bot 📖	—	—	—	—	RingHom.instRingHomClass Submodule.ne_bot_iff Ideal.comap_ne_bot_of_integral_mem IsIntegralClosure.isIntegral
eq_bot_of_comap_eq_bot 📖	—	Ideal.comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	—	Mathlib.Tactic.Contrapose.contrapose₁ RingHom.instRingHomClass comap_ne_bot
isMaximal_of_isMaximal_comap 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring	—	RingHom.instRingHomClass IsIntegralClosure.isIntegral_algebra Ideal.isMaximal_of_isIntegral_of_isMaximal_comap

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isMaximal_liesOver 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.over_def Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
of_liesOver_isMaximal 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring	—	Ideal.isMaximal_of_isIntegral_of_isMaximal_comap Ideal.over_def
under 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.under	—	Ideal.isMaximal_comap_of_isIntegral_of_isMaximal

Ideal.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebra_isIntegral_of_liesOver 📖	mathematical	—	Algebra.IsIntegral HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 commRing instRingQuotient algebraOfLiesOver	—	Algebra.IsIntegral.tower_top isScalarTower_of_liesOver IsScalarTower.left instIsIntegralQuotientIdeal

Ideal.primesOver

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMaximal 📖	mathematical	—	Ideal.IsMaximal CommSemiring.toSemiring CommRing.toCommSemiring Ideal Set Set.instMembership Ideal.primesOver	—	Ideal.IsMaximal.of_liesOver_isMaximal liesOver isPrime

---

← Back to Index