NonZeroDivisors

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

Statistics

Metric	Count
Definitions	0
Theorems ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, ringKrullDim_mvPolynomial_of_isEmpty, ringKrullDim_quotient, ringKrullDim_quotient_succ_le_of_nonZeroDivisor, ringKrullDim_succ_le_of_surjective, ringKrullDim_succ_le_ringKrullDim_polynomial, ringKrullDim_succ_le_ringKrullDim_powerseries	8
Total	8

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ringKrullDim CommRing.toCommSemiring WithBot.some ENat.card MvPolynomial MvPolynomial.commSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim ringKrullDim_eq_bot_of_subsingleton Unique.instSubsingleton finite_or_infinite ENat.card_eq_coe_natCard ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial ENat.card_eq_top_of_infinite WithBot.eq_top_iff_forall_ge instNoTopOrderOfNoMaxOrder Nat.instNoMaxOrder Function.invFun_surjective Function.Embedding.inj' Fin.val_injective le_trans Nat.card_eq_fintype_card Fintype.card_fin Nat.cast_add Nat.cast_one WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithTop.zeroLEOneClass Nat.instZeroLEOneClass WithTop.charZero Nat.instCharZero IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd WithBot.le_add_self LT.lt.ne' Order.bot_lt_krullDim PrimeSpectrum.instNonemptyOfNontrivial Finite.of_fintype ringKrullDim_le_of_surjective MvPolynomial.rename_surjective
ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ringKrullDim CommRing.toCommSemiring AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Nat.card MvPolynomial MvPolynomial.commSemiring	—	Finite.induction_empty_option Nat.card_congr ringKrullDim_eq_of_ringEquiv Nat.card_eq_fintype_card Fintype.card_eq_zero PEmpty.instIsEmpty CharP.cast_eq_zero CharP.ofCharZero WithBot.charZero add_zero ringKrullDim_mvPolynomial_of_isEmpty Fintype.card_option Nat.cast_add Nat.cast_one le_imp_le_of_le_of_le add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid le_refl ringKrullDim_succ_le_ringKrullDim_polynomial Eq.ge
ringKrullDim_mvPolynomial_of_isEmpty 📖	mathematical	—	ringKrullDim MvPolynomial CommRing.toCommSemiring MvPolynomial.commSemiring	—	ringKrullDim_eq_of_ringEquiv
ringKrullDim_quotient 📖	mathematical	—	ringKrullDim HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.commSemiring Order.krullDim Set.Elem PrimeSpectrum PrimeSpectrum.zeroLocus SetLike.coe Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Subtype.preorder PartialOrder.toPreorder PrimeSpectrum.instPartialOrder Set Set.instMembership	—	ringKrullDim.eq_1 Order.krullDim_eq_of_orderIso
ringKrullDim_quotient_succ_le_of_nonZeroDivisor 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instCommSemiringENat ringKrullDim HasQuotient.Quotient Ideal Ideal.instHasQuotient_1 Ideal.span Set Set.instSingletonSet Ideal.Quotient.commSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	ringKrullDim_eq_bot_of_subsingleton Unique.instSubsingleton Set.nonempty_coe_sort Set.nonempty_iff_ne_empty PrimeSpectrum.zeroLocus_empty_iff_eq_top Ideal.Quotient.nontrivial_iff RingHom.domain_nontrivial Ideal.instIsTwoSided_1 ringKrullDim_quotient Order.krullDim_eq_iSup_length ringKrullDim.eq_1 PrimeSpectrum.instNonemptyOfNontrivial WithBot.coe_one WithBot.coe_add ENat.iSup_add RelSeries.instNonempty WithBot.coe_le_coe iSup_le_iff Ideal.exists_minimalPrimes_le PrimeSpectrum.isPrime bot_le lt_of_le_of_ne Set.disjoint_iff Ideal.disjoint_nonZeroDivisors_of_mem_minimalPrimes PrimeSpectrum.zeroLocus_span le_trans RelSeries.cons_length Nat.cast_add Nat.cast_one le_iSup
ringKrullDim_succ_le_of_surjective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike nonZeroDivisors MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring instCommSemiringENat ringKrullDim WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	le_trans add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid ringKrullDim_le_of_surjective Ideal.instIsTwoSided_1 RingHom.instRingHomClass Ideal.span_singleton_le_iff_mem Ideal.Quotient.lift_surjective_of_surjective ringKrullDim_quotient_succ_le_of_nonZeroDivisor
ringKrullDim_succ_le_ringKrullDim_polynomial 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ringKrullDim CommRing.toCommSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Polynomial Polynomial.commSemiring	—	ringKrullDim_succ_le_of_surjective Polynomial.coeff_C_zero Polynomial.X_mem_nonzeroDivisors Polynomial.coeff_X_zero
ringKrullDim_succ_le_ringKrullDim_powerseries 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ringKrullDim CommRing.toCommSemiring WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne PowerSeries PowerSeries.instCommSemiring	—	ringKrullDim_succ_le_of_surjective MvPowerSeries.X_mem_nonzeroDivisors PowerSeries.constantCoeff_X

---

← Back to Index