KrullsHeightTheorem

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

Statistics

Metric	Count
Definitions	0
Theorems exists_finset_card_eq_height_of_isNoetherianRing, exists_spanRank_eq_and_height_eq, finiteHeight_of_isNoetherianRing, height_eq_height_add_of_liesOver_of_hasGoingDown, height_le_card_of_mem_minimalPrimes_span, height_le_card_of_mem_minimalPrimes_span_finset, height_le_height_add_encard_of_subset, height_le_height_add_of_liesOver, height_le_height_add_one_of_mem, height_le_height_add_spanFinrank_of_le, height_le_iff_exists_minimalPrimes, height_le_one_of_isPrincipal_of_mem_minimalPrimes, height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing, height_le_ringKrullDim_quotient_add_encard, height_le_ringKrullDim_quotient_add_one, height_le_spanFinrank, height_le_spanRank, height_le_spanRank_toENat, height_le_spanRank_toENat_of_mem_minimal_primes, map_height_le_one_of_mem_minimalPrimes, mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert, quotient_artinian_of_mem_minimalPrimes_of_isLocalRing, height_le_ringKrullDim_quotient_add_spanFinrank, instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing, ringKrullDim_le_ringKrullDim_quotient_add_card, ringKrullDim_le_ringKrullDim_quotient_add_encard, ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank, ringKrullDim_le_spanFinrank_maximalIdeal	28
Total	28

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finset_card_eq_height_of_isNoetherianRing 📖	mathematical	—	Finset Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes span SetLike.coe Finset.instSetLike ENat ENat.instNatCast Finset.card height	—	height_le_iff_exists_minimalPrimes le_rfl Submodule.FG.finite_generators IsNoetherian.noetherian Set.Finite.coe_toFinset span.eq_1 Submodule.span_generators Set.ncard_eq_toFinset_card Submodule.FG.generators_ncard le_antisymm Cardinal.nat_le_ofENat Submodule.fg_iff_spanRank_eq_spanFinrank height_le_spanRank_toENat_of_mem_minimal_primes
exists_spanRank_eq_and_height_eq 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.spanRank Cardinal.ofENat height	—	exists_spanRank_le_and_le_height_of_le_height ENat.coe_toNat_le_self le_antisymm Cardinal.ofENat_eq_nat ENat.coe_toNat height_ne_top finiteHeight_of_isNoetherianRing le_trans Cardinal.ofENat_le_ofENat_of_le ENat.coe_toNat_eq_self height_le_spanRank top_le_iff height_mono
finiteHeight_of_isNoetherianRing 📖	mathematical	—	FiniteHeight	—	finiteHeight_iff_lt em LE.le.trans_lt height_le_spanFinrank ENat.coe_lt_top
height_eq_height_add_of_liesOver_of_hasGoingDown 📖	mathematical	—	height ENat instAddENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Quotient.commRing Quotient.ring instIsTwoSided_1	—	le_antisymm instIsTwoSided_1 height_le_height_add_of_liesOver exists_ltSeries_length_eq_height finiteHeight_of_isNoetherianRing Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver Quotient.isNoetherianRing RingHom.strictMono_comap_of_surjective Quotient.mk_surjective map_le_iff_le_comap RingHom.instRingHomClass PrimeSpectrum.comap_asIdeal map_quotient_self LiesOver.over under_def comap_mono le_trans LTSeries.head_le_last comap.congr_simp comap_map_quotientMk sup_of_le_right instReflLe PrimeSpectrum.isPrime exists_ltSeries_of_hasGoingDown Nat.cast_add height_eq_primeHeight Order.length_le_height RelSeries.last_smash
height_le_card_of_mem_minimalPrimes_span 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes span	ENat instLEENat height ENat.instNatCast Set.ncard	—	Set.ncard_eq_toFinset_card height_le_card_of_mem_minimalPrimes_span_finset Set.Finite.coe_toFinset
height_le_card_of_mem_minimalPrimes_span_finset 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes span SetLike.coe Finset Finset.instSetLike	ENat instLEENat height ENat.instNatCast Finset.card	—	height_le_spanRank_toENat_of_mem_minimal_primes Cardinal.mk_fintype Fintype.card_coe Submodule.spanRank_span_le_card
height_le_height_add_encard_of_subset 📖	mathematical	Set Set.instHasSubset SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	ENat instLEENat height instAddENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient span Quotient.commRing map RingHom Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Set.encard	—	le_trans instIsTwoSided_1 height_le_height_add_spanFinrank_of_le span_le add_le_add_right IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Submodule.spanFinrank_span_le_encard
height_le_height_add_of_liesOver 📖	mathematical	—	ENat instLEENat height instAddENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient map RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap Quotient.commRing Quotient.ring instIsTwoSided_1	—	instIsTwoSided_1 exists_finset_card_eq_height_of_isNoetherianRing Quotient.isNoetherianRing Quotient.instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver subset_span Set.SurjOn.mono subset_rfl Set.instReflSubset Quotient.mk_surjective mem_quotient_iff_mem RingHom.instRingHomClass map_le_iff_le_comap LiesOver.over le_refl SetLike.mem_coe Finset.exists_subset_injOn_image_eq_of_surjOn height_le_card_of_mem_minimalPrimes_span_finset Finset.coe_union Finset.coe_image span_union map_span map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes span_le le_trans IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Finset.card_union_le add_le_add Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Finset.card_image_le Finset.card_image_of_injOn
height_le_height_add_one_of_mem 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	ENat instLEENat height instAddENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient span Set Set.instSingletonSet Quotient.commRing map RingHom Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	instIsTwoSided_1 Set.encard_singleton height_le_height_add_encard_of_subset
height_le_height_add_spanFinrank_of_le 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	ENat instLEENat height instAddENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient Quotient.commRing map RingHom Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike ENat.instNatCast Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	isPrime_map_quotientMk_of_isPrime instIsTwoSided_1 exists_finset_card_eq_height_of_isNoetherianRing Quotient.isNoetherianRing subset_span Set.SurjOn.mono subset_rfl Set.instReflSubset Quotient.mk_surjective sup_of_le_left Finset.exists_subset_injOn_image_eq_of_surjOn IsNoetherian.noetherian Submodule.FG.finite_generators height_le_card_of_mem_minimalPrimes_span_finset Finset.coe_union Set.Finite.coe_toFinset span_union sup_comm span.eq_1 Submodule.span_generators mem_minimalPrimes_sup map_span RingHom.instRingHomClass Finset.coe_image le_trans IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Set.ncard_eq_toFinset_card Submodule.FG.generators_ncard
height_le_iff_exists_minimalPrimes 📖	mathematical	—	ENat instLEENat height Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes Cardinal Cardinal.instLE Submodule.spanRank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Cardinal.ofENat	—	exists_spanRank_eq_and_height_eq IsPrime.ne_top mem_minimalPrimes_of_height_eq finiteHeight_of_isNoetherianRing Eq.ge le_trans height_le_spanRank_toENat_of_mem_minimal_primes MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass OrderRingHom.instRingHomClass OrderRingHom.toRingHom_eq_coe Cardinal.toENat_ofENat OrderRingHom.monotone'
height_le_one_of_isPrincipal_of_mem_minimalPrimes 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes	ENat instLEENat height AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Localization.AtPrime.isLocalRing height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing IsLocalization.instIsNoetherianRingLocalization instIsPrincipalMapRingHom RingHom.instRingHomClass IsLocalization.minimalPrimes_map Localization.isLocalization Set.mem_preimage Localization.AtPrime.comap_maximalIdeal IsLocalization.height_comap
height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes IsLocalRing.maximalIdeal	ENat instLEENat height IsLocalRing.maximalIdeal CommRing.toCommSemiring AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_le_iff IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal IsLocalization.AtPrime.ringKrullDim_eq_height Localization.isLocalization WithBot.coe_zero ringKrullDimZero_iff_ringKrullDim_eq_zero IsLocalRing.toNontrivial Localization.AtPrime.isLocalRing isArtinianRing_iff_krullDimLE_zero IsLocalization.instIsNoetherianRingLocalization IsScalarTower.right isArtinianRing_iff_isNilpotent_maximalIdeal Localization.AtPrime.map_eq_maximalIdeal IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing instIsTwoSided_1 RingHom.instRingHomClass map_mono comap_mono pow_le_pow_right IsArtinian.monotone_stabilizes Submodule.eq_bot_of_le_smul_of_le_jacobson_bot IsNoetherian.noetherian IsScalarTower.left smul_eq_mul pow_succ' RelEmbedding.map_rel_iff Submodule.le_of_le_smul_of_le_jacobson_bot IsLocalRing.jacobson_eq_maximalIdeal bot_ne_top instNontrivial Submodule.mem_sup Eq.le comap_map_of_surjective Quotient.mk_surjective mk_ker mem_sup_left Submodule.add_mem_sup Submodule.IsPrincipal.mem_iff_eq_smul_generator mul_comm mul_mem_mul unit_mul_mem_iff_mem IsLocalization.map_units Submodule.IsPrincipal.principal Set.singleton_subset_iff span_le span_singleton_generator LT.lt.not_ge LT.lt.le add_mem_iff_right RingHom.map_mul RingHom.map_add mem_comap Submodule.IsPrincipal.generator_mem le_refl zero_lt_one NeZero.charZero_one
height_le_ringKrullDim_quotient_add_encard 📖	mathematical	Set Set.instHasSubset SetLike.coe Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.some height WithBot.add instAddENat ringKrullDim HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 span Quotient.commSemiring Set.encard	—	le_trans height_le_ringKrullDim_quotient_add_spanFinrank add_le_add_right WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Submodule.spanFinrank_span_le_encard
height_le_ringKrullDim_quotient_add_one 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.some height WithBot.add instAddENat ringKrullDim HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring instHasQuotient_1 span Set Set.instSingletonSet Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Set.encard_singleton height_le_ringKrullDim_quotient_add_encard
height_le_spanFinrank 📖	mathematical	—	ENat instLEENat height ENat.instNatCast Submodule.spanFinrank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Submodule.fg_iff_spanRank_eq_spanFinrank IsNoetherian.noetherian map_natCast OrderRingHom.instRingHomClass height_le_spanRank_toENat
height_le_spanRank 📖	mathematical	—	Cardinal Cardinal.instLE Cardinal.ofENat height Submodule.spanRank CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	height_le_spanRank_toENat Cardinal.ofENat_toENat_le
height_le_spanRank_toENat 📖	mathematical	—	ENat instLEENat height DFunLike.coe OrderRingHom Cardinal Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat instPreorderENat OrderRingHom.instFunLike Cardinal.toENat Submodule.spanRank CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	nonempty_minimalPrimes LE.le.trans iInf₂_le height_eq_primeHeight height_le_spanRank_toENat_of_mem_minimal_primes
height_le_spanRank_toENat_of_mem_minimal_primes 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes	ENat instLEENat height DFunLike.coe OrderRingHom Cardinal Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring PartialOrder.toPreorder Cardinal.partialOrder instCommSemiringENat instPreorderENat OrderRingHom.instFunLike Cardinal.toENat Submodule.spanRank CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Submodule.spanRank_toENat_eq_iInf_finset_card le_iInf_iff Nat.strong_induction_on Eq.le ENat.coe_zero nonpos_iff_eq_zero height_eq_primeHeight primeHeight_eq_zero_iff minimalPrimes.eq_1 Nat.instCanonicallyOrderedAdd Finset.coe_empty span_empty span_le lt_irrefl LE.le.trans_lt LT.lt.le Set.not_subset Finset.mem_erase Finset.insert_erase radical_eq_sInf le_sInf_iff by_contra LT.lt.trans_le SetLike.lt_iff_le_and_exists instIsConcreteLE le_sup_left mem_sup_right mem_span_singleton_self LE.le.lt_of_not_ge IsLocalRing.le_maximalIdeal IsPrime.ne_top LE.le.trans Set.insert_subset_iff Finset.coe_insert exists_subset_radical_span_sup_of_subset_radical_sup Finset.coe_image Finset.coe_attach Set.image_univ mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert HasSubset.Subset.trans Set.instIsTransSubset radical_mono Set.union_singleton span_union le_refl Finset.card_image_le Finset.card_attach Finset.card_lt_card Finset.ssubset_insert IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid RingHom.instRingHomClass Localization.AtPrime.isLocalRing Localization.AtPrime.comap_maximalIdeal IsLocalization.height_comap Localization.isLocalization IsLocalization.instIsNoetherianRingLocalization map_span IsLocalization.minimalPrimes_map Set.mem_preimage IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal
map_height_le_one_of_mem_minimalPrimes 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id span Set.instSingletonSet	ENat instLEENat height HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient Quotient.commRing map RingHom Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	instIsTwoSided_1 RingHom.instRingHomClass Eq.trans_le mk_ker LE.le.trans le_sup_left height_le_one_of_isPrincipal_of_mem_minimalPrimes Quotient.isNoetherianRing instIsPrincipalMapRingHom instIsPrincipalSpanSingletonSet map_isPrime_of_surjective Quotient.mk_surjective map_mono le_sup_right map_le_iff_le_comap IsPrime.comap sup_le_iff ker_le_comap le_comap_of_map_le comap_mono Eq.le comap_map_of_surjective sup_eq_left
mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Set Set.instMembership minimalPrimes span Set.instInsert Set.instHasSubset SetLike.coe Submodule.setLike radical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes span	—	instIsTwoSided_1 Quotient.mk_surjective span_le LE.le.trans LT.lt.le minimalPrimes_isPrime map_isPrime_of_surjective RingHom.instRingHomClass mk_ker height_le_one_of_isPrincipal_of_mem_minimalPrimes Quotient.isNoetherianRing instIsPrincipalMapRingHom instIsPrincipalSpanSingletonSet map_mono Set.singleton_subset_iff subset_span map_le_iff_le_comap IsPrime.comap Set.insert_subset_iff HasSubset.Subset.trans Set.instIsTransSubset IsRadical.radical_le_iff IsPrime.isRadical Eq.trans_le ker_le_comap sup_eq_left RingHom.ker_eq_comap_bot comap_map_of_surjective comap_mono LE.le.lt_of_not_ge LT.lt.not_ge LT.lt.ne LE.le.trans_lt WithTop.coe_lt_top LT.lt.trans_le primeHeight_strict_mono height_eq_primeHeight minimal_primes_comap_of_surjective primeHeight_eq_zero_iff ENat.lt_one_iff_eq_zero

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotient_artinian_of_mem_minimalPrimes_of_isLocalRing 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership Ideal.minimalPrimes maximalIdeal	IsArtinianRing HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring	—	Ring.krullDimLE_zero_iff Ideal.isMaximal_of_isIntegral_of_isMaximal_comap instIsIntegralQuotientIdeal Algebra.IsIntegral.of_finite Module.Finite.self RingHom.instRingHomClass Ideal.instIsTwoSided_1 Ideal.IsPrime.comap Minimal.eq_of_le Set.mem_setOf Ideal.minimalPrimes.eq_1 LE.le.trans Ideal.mk_ker instReflLe Ideal.ker_le_comap le_maximalIdeal Ideal.IsPrime.ne_top' maximalIdeal.isMaximal IsNoetherianRing.isArtinianRing_of_krullDimLE_zero Ideal.Quotient.isNoetherianRing

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_le_ringKrullDim_quotient_add_spanFinrank 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.some Ideal.height WithBot.add instAddENat ringKrullDim HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring WithBot.natCast ENat.instNatCast Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Ideal.instIsTwoSided_1 Ideal.height_le_height_add_spanFinrank_of_le add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Ideal.isPrime_map_quotientMk_of_isPrime Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'
instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing 📖	mathematical	—	FiniteRingKrullDim CommRing.toCommSemiring	—	finiteRingKrullDim_iff_ne_bot_and_top IsLocalRing.maximalIdeal_height_eq_ringKrullDim WithBot.coe_ne_bot WithBot.coe_top Ideal.finiteHeight_iff Ideal.finiteHeight_of_isNoetherianRing Ideal.IsPrime.ne_top' Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal
ringKrullDim_le_ringKrullDim_quotient_add_card 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Ideal Ring.toSemiring CommRing.toRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.jacobson	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat ringKrullDim CommRing.toCommSemiring WithBot.add instAddENat HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.span SetLike.coe Finset Finset.instSetLike Ideal.Quotient.commSemiring WithBot.natCast ENat.instNatCast Finset.card	—	Set.encard_coe_eq_coe_finsetCard ringKrullDim_le_ringKrullDim_quotient_add_encard
ringKrullDim_le_ringKrullDim_quotient_add_encard 📖	mathematical	Set Set.instHasSubset SetLike.coe Ideal Ring.toSemiring CommRing.toRing Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.jacobson	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat ringKrullDim CommRing.toCommSemiring WithBot.add instAddENat HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.span Ideal.Quotient.commSemiring WithBot.some Set.encard	—	le_trans ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank add_le_add_right WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid Submodule.spanFinrank_span_le_encard
ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.jacobson CommRing.toRing	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat ringKrullDim CommRing.toCommSemiring WithBot.add instAddENat HasQuotient.Quotient Ideal CommSemiring.toSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring WithBot.natCast ENat.instNatCast Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim ringKrullDim_eq_bot_of_subsingleton Submodule.Quotient.instSubsingletonQuotient instReflLe ringKrullDim_le_iff_isMaximal_height_le height_le_ringKrullDim_quotient_add_spanFinrank Ideal.IsMaximal.isPrime' le_trans Ring.jacobson_le_of_isMaximal
ringKrullDim_le_spanFinrank_maximalIdeal 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat ringKrullDim CommRing.toCommSemiring WithBot.natCast ENat.instNatCast Submodule.spanFinrank CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	—	IsLocalRing.maximalIdeal_height_eq_ringKrullDim WithBot.coe_le_coe Ideal.height_le_spanFinrank Ideal.IsPrime.ne_top' Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal

---

← Back to Index