Regular

📁 Source: Mathlib/RingTheory/KrullDimension/Regular.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_ltSeries_support_isMaximal_last_of_ltSeries_support, ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors, supportDim_add_length_eq_supportDim_of_isRegular, supportDim_le_supportDim_quotSMulTop_succ, supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, supportDim_quotSMulTop_succ_eq_supportDim, supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, ringKrullDim_add_length_eq_ringKrullDim_of_isRegular, ringKrullDim_le_ringKrullDim_add_card, ringKrullDim_le_ringKrullDim_add_spanFinrank, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson, ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors	19
Total	19

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_ltSeries_support_isMaximal_last_of_ltSeries_support 📖	mathematical	—	RelSeries.length Set.Elem PrimeSpectrum CommRing.toCommSemiring support setOf Preorder.toLT Subtype.preorder PartialOrder.toPreorder PrimeSpectrum.instPartialOrder Set Set.instMembership Ideal.IsMaximal CommSemiring.toSemiring PrimeSpectrum.asIdeal RelSeries.last	—	Ideal.exists_le_maximal Ideal.IsPrime.ne_top' PrimeSpectrum.isPrime lt_or_eq_of_le Ideal.IsMaximal.isPrime' mem_support_mono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd RelSeries.last_snoc le_refl
ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors WithBot.some ENat Ideal.height ringKrullDim Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	WithBot WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_antisymm ringKrullDim_quotient_succ_le_of_nonZeroDivisor Ideal.height_le_ringKrullDim_quotient_add_one
supportDim_add_length_eq_supportDim_of_isRegular 📖	mathematical	RingTheory.Sequence.IsRegular	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat supportDim HasQuotient.Quotient Submodule CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient CommRing.toRing Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid toDistribMulAction Ideal.ofList Top.top Submodule.instTop Submodule.Quotient.addCommGroup Submodule.Quotient.module AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.left Ideal.ofList_nil Submodule.bot_smul CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero add_zero supportDim_eq_of_equiv RingTheory.Sequence.IsRegular.top_ne_smul Ideal.ofList_cons Ideal.span_singleton_eq_top sup_of_le_left Submodule.top_smul Submodule.Quotient.isScalarTower Nat.cast_add Nat.cast_one supportDim_quotSMulTop_succ_eq_supportDim RingTheory.Sequence.isRegular_cons_iff Finite.quotient
supportDim_le_supportDim_quotSMulTop_succ 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat supportDim WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson IsLocalRing.maximalIdeal_le_jacobson
supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson 📖	mathematical	Ideal Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson annihilator CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat supportDim WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat QuotSMulTop Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim supportDim_eq_bot_of_subsingleton Submodule.Quotient.instSubsingletonQuotient iSup_le_iff PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last supportDim_ne_bot_iff_nontrivial Submodule.Quotient.nontrivial_iff smulCommClass_self Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator WithBot.coe_unbot WithBot.coe_le_coe zero_le LT.lt.trans_eq support_quotSMulTop mem_support_mono LTSeries.monotone Eq.trans_le LTSeries.strictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass le_imp_le_of_le_of_le Nat.mono_cast WithBot.addLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithBot.zeroLEOneClass IsOrderedRing.toZeroLEOneClass le_tsub_add Nat.instOrderedSub le_refl Nat.cast_add_one supportDim.eq_1 Order.krullDim.eq_1 add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add le_iSup exists_ltSeries_support_isMaximal_last_of_ltSeries_support sInf_le mem_support_iff_of_finite LE.le.trans Nat.cast_le WithBot.charZero
supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.toSemiring CommRing.toRing Ideal.jacobson annihilator AddCommGroup.toAddCommMonoid	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat supportDim QuotSMulTop Submodule.Quotient.addCommGroup Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_antisymm supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson
supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat supportDim QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson IsLocalRing.maximalIdeal_le_jacobson
supportDim_quotSMulTop_succ_eq_supportDim 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toDistribMulAction AddCommGroup.toAddCommMonoid Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat supportDim QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson IsLocalRing.maximalIdeal_le_jacobson
supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson 📖	mathematical	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring toDistribMulAction AddCommGroup.toAddCommMonoid Ideal Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson annihilator	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat supportDim QuotSMulTop Submodule.Quotient.addCommGroup Submodule AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid Submodule.pointwiseDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson IsSMulRegular.notMem_of_mem_minimalPrimes
supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes 📖	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.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat supportDim QuotSMulTop Submodule.Quotient.addCommGroup CommRing.toRing Submodule AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction toDistribMulAction Top.top Submodule.instTop Submodule.Quotient.module WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim supportDim_eq_bot_of_subsingleton Submodule.Quotient.instSubsingletonQuotient Set.Nonempty.to_subtype nonempty_support_of_nontrivial Order.krullDim_eq_iSup_length WithBot.coe_le_coe ENat.iSup_add RelSeries.instNonempty support_quotSMulTop Ideal.exists_minimalPrimes_le PrimeSpectrum.isPrime mem_support_iff_of_finite Ideal.minimalPrimes_isPrime lt_of_le_of_ne RelSeries.cons_length Nat.cast_add Nat.cast_one le_iSup

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringKrullDim_add_length_eq_ringKrullDim_of_isRegular 📖	mathematical	RingTheory.Sequence.IsRegular Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.ofList Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	IsScalarTower.right Ideal.mul_top Ideal.instIsTwoSided_1 ringKrullDim_eq_of_ringEquiv Module.supportDim_quotient_eq_ringKrullDim Module.supportDim_self_eq_ringKrullDim Module.supportDim_add_length_eq_supportDim_of_isRegular Module.Finite.self
ringKrullDim_le_ringKrullDim_add_card 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ringKrullDim WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Finset.card	—	ringKrullDim_le_ringKrullDim_quotient_add_card IsLocalRing.ringJacobson_eq_maximalIdeal
ringKrullDim_le_ringKrullDim_add_spanFinrank 📖	mathematical	—	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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Submodule.spanFinrank NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule	—	ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank IsLocalRing.ringJacobson_eq_maximalIdeal IsLocalRing.le_maximalIdeal
ringKrullDim_le_ringKrullDim_quotSMulTop_succ 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ringKrullDim WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat HasQuotient.Quotient Ideal.instHasQuotient_1 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.to_smulCommClass Algebra.id Top.top Submodule.instTop Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass Module.supportDim_self_eq_ringKrullDim Module.supportDim_quotient_eq_ringKrullDim Module.supportDim_le_supportDim_quotSMulTop_succ Module.Finite.self
ringKrullDim_quotSMulTop_succ_eq_ringKrullDim 📖	mathematical	IsSMulRegular Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim QuotSMulTop Ring.toAddCommGroup CommRing.toRing Ideal.Quotient.commSemiring Submodule AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson IsLocalRing.ringJacobson_eq_maximalIdeal
ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson 📖	mathematical	IsSMulRegular Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Ideal Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.jacobson	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim QuotSMulTop Ring.toAddCommGroup Ideal.Quotient.commSemiring Submodule AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Submodule.pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Submodule.pointwiseDistribMulAction Module.toDistribMulAction Top.top Submodule.instTop WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Module.supportDim_quotient_eq_ringKrullDim Module.supportDim_self_eq_ringKrullDim Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson Module.Finite.self Ideal.ringJacobson_le_jacobson
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim 📖	mathematical	IsSMulRegular Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Ideal SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson IsLocalRing.ringJacobson_eq_maximalIdeal
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson 📖	mathematical	IsSMulRegular Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Ideal Ring.toSemiring CommRing.toRing SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ring.jacobson	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Algebra.to_smulCommClass smulCommClass_self IsScalarTower.left Ideal.mul_top Ideal.instIsTwoSided_1 ringKrullDim_eq_of_ringEquiv ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson
ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors Ideal Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing.maximalIdeal	WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim Module.Flat.isSMulRegular_of_nonZeroDivisors Module.FaithfullyFlat.toFlat Module.FaithfullyFlat.instOfNontrivialOfFree IsLocalRing.toNontrivial Module.Free.self

---

← Back to Index