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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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₂	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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₂	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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 📖	mathematical	comap RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass Bot.bot Ideal Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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₂	Set Set.instMembership Set.instSDiff SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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₂	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule 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	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring IsMaximal 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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring IsMaximal comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsPrime comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring IsPrime comap RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsPrime comap RingHom RingHom.instFunLike algebraMap RingHom.instRingHomClass	—	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	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring IsMaximal 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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring 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 CommSemiring.toSemiring CommRing.toCommSemiring Ideal Ring.toSemiring Polynomial.ring CommRing.toRing instHasQuotient comap RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RingHom.instRingHomClass Quotient.semiring Quotient.instRingQuotient map Polynomial.mapRingHom instIsTwoSided_1 DFunLike.coe Quotient.ring 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 CommSemiring.toSemiring CommRing.toCommSemiring	—	primesOver.isMaximal
map_eq_top_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike RingHom.IsIntegral CommRing.toRing	map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike 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 RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Top.top Ideal Submodule.instTop NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	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 📖	mathematical	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	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	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.semiring Polynomial.ring Quotient.instRingQuotient map Polynomial.mapRingHom instIsTwoSided_1 Quotient.ring 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 CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.comap Subalgebra SetLike.instMembership Subalgebra.instSetLike integralClosure RingHom Subalgebra.toSemiring 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 📖	mathematical	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	Bot.bot Ideal Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike integralClosure Subalgebra.toSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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 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 📖	mathematical	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	Bot.bot Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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