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	27
Total	27

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_finset_card_eq_height_of_isNoetherianRing 📖	mathematical	—	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Set Set.instMembership minimalPrimes span SetLike.coe Finset 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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient map RingHom 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 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient span Quotient.commRing map RingHom Quotient.ring instIsTwoSided_1 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat HasQuotient.Quotient Ideal Ring.toSemiring CommRing.toRing instHasQuotient map RingHom 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 IsOrderedRing.toZeroLEOneClass 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient span Set Set.instSingletonSet Quotient.commRing map RingHom Quotient.ring instIsTwoSided_1 RingHom.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient Quotient.commRing map RingHom Quotient.ring instIsTwoSided_1 RingHom.instFunLike ENat.instNatCast Submodule.spanFinrank	—	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 IsOrderedRing.toZeroLEOneClass Set.ncard_eq_toFinset_card Submodule.FG.generators_ncard
height_le_iff_exists_minimalPrimes 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring instCommSemiringENat	—	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 IsOrderedRing.toZeroLEOneClass 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 PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.some height WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient 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 PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.some height WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient instHasQuotient_1 span Set Set.instSingletonSet Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Set.encard_singleton height_le_ringKrullDim_quotient_add_encard
height_le_spanFinrank 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height DFunLike.coe OrderRingHom Cardinal Semiring.toNonAssocSemiring CommSemiring.toSemiring Cardinal.commSemiring Cardinal.partialOrder instCommSemiringENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height DFunLike.coe OrderRingHom Cardinal Semiring.toNonAssocSemiring Cardinal.commSemiring Cardinal.partialOrder instCommSemiringENat SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat OrderRingHom.instFunLike Cardinal.toENat Submodule.spanRank 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 IsOrderedRing.toZeroLEOneClass 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 Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat height HasQuotient.Quotient Ring.toSemiring CommRing.toRing instHasQuotient Quotient.commRing map RingHom Semiring.toNonAssocSemiring Quotient.ring instIsTwoSided_1 RingHom.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instCommSemiringENat	—	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 📖	—	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	—	—	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.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 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 WithBot.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.some Ideal.height WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Submodule.spanFinrank	—	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 PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ringKrullDim CommRing.toCommSemiring WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib CommSemiring.toSemiring instCommSemiringENat HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne 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 PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ringKrullDim CommRing.toCommSemiring WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib CommSemiring.toSemiring instCommSemiringENat HasQuotient.Quotient 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 WithBot.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ringKrullDim WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Submodule.spanFinrank	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim ringKrullDim_eq_bot_of_subsingleton Submodule.Quotient.instSubsingletonQuotient ringKrullDim_le_iff_isMaximal_height_le height_le_ringKrullDim_quotient_add_spanFinrank Ideal.IsMaximal.isPrime' le_trans Ring.jacobson_le_of_isMaximal

---

← Back to Index