Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `FiniteRingKrullDim`, `KrullDimLE`, `ringKrullDim`	3
Theorems `isMaximal'`, `isMaximal_iff_isPrime`, `isMaximal_of_isPrime`, `mem_minimalPrimes_iff_isPrime`, `mem_minimalPrimes_of_krullDimLE_zero`, `of_finiteRingKrullDim`, `mk₀`, `mk₁`, `mk₁'`, `jacobson_eq_nilradical_of_krullDimLE_zero`, `krullDimLE_iff`, `krullDimLE_one_iff`, `krullDimLE_one_iff_of_isPrime_bot`, `krullDimLE_one_iff_of_noZeroDivisors`, `krullDimLE_zero_iff`, `ringKrullDim`, `finiteRingKrullDim_iff_ne_bot_and_top`, `instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat`, `instKrullDimLEOfNatNat`, `nilradical_le_jacobson`, `ringKrullDim_eq_bot_of_subsingleton`, `ringKrullDim_eq_of_ringEquiv`, `ringKrullDim_le_of_surjective`, `ringKrullDim_lt_top`, `ringKrullDim_ne_bot`, `ringKrullDim_ne_top`, `ringKrullDim_nonneg_of_nontrivial`, `ringKrullDim_quotient_le`	28
Total	31

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal_iff_isPrime` 📖	mathematical	—	`IsMaximal` `CommSemiring.toSemiring` `IsPrime`	—	`IsMaximal.isPrime` `instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat`
`isMaximal_of_isPrime` 📖	mathematical	—	`IsMaximal` `CommSemiring.toSemiring`	—	`Ring.krullDimLE_zero_iff`
`mem_minimalPrimes_iff_isPrime` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `IsPrime`	—	`mem_minimalPrimes_of_krullDimLE_zero`
`mem_minimalPrimes_of_krullDimLE_zero` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes`	—	`Eq.ge` `IsMaximal.eq_of_le` `instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat` `IsPrime.ne_top'` `minimalPrimes_eq_minimals`

Ideal.IsPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMaximal'` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring`	—	`Ideal.isMaximal_of_isPrime`

Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finiteRingKrullDim` 📖	mathematical	—	`Nontrivial`	—	`PrimeSpectrum.nonempty_iff_nontrivial` `LTSeries.nonempty_of_finiteDimensionalOrder`

Ring

Definitions

Name	Category	Theorems
`KrullDimLE` 📖	MathDef	19 math math: `PrimeSpectrum.discreteTopology_iff_finite_and_krullDimLE_zero`, `krullDimLE_iff`, `KrullDimLE.mk₁'`, `IsPrincipalIdealRing.krullDimLE_one`, `krullDimLE_zero_and_isLocalRing_tfae`, `ringKrullDimZero_iff_ringKrullDim_eq_zero`, `isArtinianRing_iff_isNoetherianRing_krullDimLE_zero`, `KrullDimLE.mk₀`, `krullDimLE_one_iff_of_noZeroDivisors`, `krullDimLE_zero_iff`, `krullDimLE_one_iff`, `KrullDimLE.of_isMaximal_nilradical`, `KrullDimLE.of_isLocalization`, `PrimeSpectrum.instKrullDimLEOfNatNat`, `Module.finite_iff_krullDimLE_zero`, `KrullDimLE.mk₁`, `isArtinianRing_iff_krullDimLE_zero`, `krullDimLE_one_iff_of_isPrime_bot`, `instKrullDimLEOfNatNat`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_eq_nilradical_of_krullDimLE_zero` 📖	mathematical	—	`jacobson` `CommRing.toRing` `nilradical` `CommRing.toCommSemiring`	—	`LE.le.antisymm'` `nilradical_le_jacobson` `le_sInf` `sInf_le` `Ideal.IsMaximal.out` `instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat` `nilradical_eq_sInf`
`krullDimLE_iff` 📖	mathematical	—	`KrullDimLE` `WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`Order.krullDimLE_iff`
`krullDimLE_one_iff` 📖	mathematical	—	`KrullDimLE` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `Ideal.IsMaximal`	—	`Nat.cast_one` `Equiv.forall_congr_left`
`krullDimLE_one_iff_of_isPrime_bot` 📖	mathematical	—	`KrullDimLE` `Ideal.IsMaximal` `CommSemiring.toSemiring`	—	`Nat.cast_one` `bot_le` `Equiv.forall_congr_left`
`krullDimLE_one_iff_of_noZeroDivisors` 📖	mathematical	—	`KrullDimLE` `Ideal.IsMaximal` `CommSemiring.toSemiring`	—	`subsingleton_or_nontrivial` `instKrullDimLEOfNatNat` `Order.instKrullDimLEOfNatNatOfSubsingleton` `IsEmpty.instSubsingleton` `PrimeSpectrum.instIsEmptyOfSubsingleton` `Unique.instSubsingleton` `krullDimLE_one_iff_of_isPrime_bot` `Ideal.isPrime_bot`
`krullDimLE_zero_iff` 📖	mathematical	—	`KrullDimLE` `Ideal.IsMaximal` `CommSemiring.toSemiring`	—	`Nat.cast_zero` `Equiv.forall_congr_left`

Ring.KrullDimLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk₀` 📖	mathematical	`Ideal.IsMaximal` `CommSemiring.toSemiring`	`Ring.KrullDimLE`	—	`Ring.krullDimLE_zero_iff`
`mk₁` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes` `Ideal.IsMaximal`	`Ring.KrullDimLE`	—	`Ring.krullDimLE_one_iff`
`mk₁'` 📖	mathematical	`Ideal.IsMaximal` `CommSemiring.toSemiring`	`Ring.KrullDimLE`	—	`Ring.krullDimLE_one_iff_of_isPrime_bot` `mk₀` `instKrullDimLEOfNatNat`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ringKrullDim` 📖	mathematical	—	`ringKrullDim`	—	`ringKrullDim_eq_of_ringEquiv`

(root)

Definitions

Name	Category	Theorems
`FiniteRingKrullDim` 📖	MathDef	2 math math: `instFiniteRingKrullDimOfIsNoetherianRingOfIsLocalRing`, `finiteRingKrullDim_iff_ne_bot_and_top`
`ringKrullDim` 📖	CompOp	57 math math: `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim`, `ringKrullDim_succ_le_ringKrullDim_polynomial`, `Ring.krullDimLE_iff`, `ringKrullDim_eq_one_iff_of_isLocalRing_isDomain`, `Module.supportDim_eq_ringKrullDim_quotient_annihilator`, `Ideal.sup_primeHeight_eq_ringKrullDim`, `ringKrullDim_quotient`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson`, `ringKrullDim_succ_le_ringKrullDim_powerseries`, `Ideal.primeHeight_eq_ringKrullDim_iff`, `ringKrullDim_eq_of_ringEquiv`, `ringKrullDim_quotSMulTop_succ_eq_ringKrullDim`, `ringKrullDim_nonneg_of_nontrivial`, `ringKrullDimZero_iff_ringKrullDim_eq_zero`, `Module.supportDim_self_eq_ringKrullDim`, `ringKrullDim_quotient_le`, `ringKrullDim_succ_le_of_surjective`, `Ideal.exists_isMaximal_height`, `Ideal.primeHeight_le_ringKrullDim`, `ringKrullDim_eq_bot_of_subsingleton`, `Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim`, `ringKrullDim_le_iff_height_le`, `ringKrullDim_le_ringKrullDim_quotient_add_card`, `Ideal.height_le_ringKrullDim_quotient_add_one`, `ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank`, `ringKrullDim_add_length_eq_ringKrullDim_of_isRegular`, `IsLocalization.AtPrime.ringKrullDim_eq_height`, `Ideal.height_le_ringKrullDim_quotient_add_encard`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors`, `ringKrullDim_quotient_succ_le_of_nonZeroDivisor`, `ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson`, `IsPrincipalIdealRing.ringKrullDim_eq_one`, `ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial`, `ringKrullDim_eq_zero_of_isField`, `ringKrullDim_le_iff_isMaximal_height_le`, `ringKrullDim_le_ringKrullDim_add_card`, `Module.supportDim_le_ringKrullDim`, `ringKrullDim_lt_top`, `Polynomial.ringKrullDim_le`, `PrimeSpectrum.topologicalKrullDim_eq_ringKrullDim`, `IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim`, `ringKrullDim_nat`, `Ideal.sup_height_eq_ringKrullDim`, `height_le_ringKrullDim_quotient_add_spanFinrank`, `ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial`, `Module.supportDim_quotient_eq_ringKrullDim`, `ringKrullDim_le_ringKrullDim_add_spanFinrank`, `IsLocalRing.maximalIdeal_height_eq_ringKrullDim`, `ringKrullDim_eq_zero_of_field`, `Polynomial.ringKrullDim_of_isNoetherianRing`, `MvPolynomial.ringKrullDim_of_isNoetherianRing`, `Ideal.height_le_ringKrullDim_of_ne_top`, `ringKrullDim_le_of_surjective`, `ringKrullDim_le_ringKrullDim_quotSMulTop_succ`, `RingEquiv.ringKrullDim`, `ringKrullDim_mvPolynomial_of_isEmpty`, `ringKrullDim_le_ringKrullDim_quotient_add_encard`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finiteRingKrullDim_iff_ne_bot_and_top` 📖	mathematical	—	`FiniteRingKrullDim`	—	`Order.finiteDimensionalOrder_iff_krullDim_ne_bot_and_top`
`instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring`	—	`Ideal.isMaximal_of_isPrime`
`instKrullDimLEOfNatNat` 📖	mathematical	—	`Ring.KrullDimLE`	—	`Order.KrullDimLE.mono` `zero_le_one` `Nat.instZeroLEOneClass`
`nilradical_le_jacobson` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nilradical` `Ring.jacobson` `CommRing.toRing`	—	`le_sInf` `sInf_le` `Ideal.IsMaximal.isPrime` `nilradical_eq_sInf`
`ringKrullDim_eq_bot_of_subsingleton` 📖	mathematical	—	`ringKrullDim` `Bot.bot` `WithBot` `ENat` `WithBot.bot`	—	`Order.krullDim_eq_bot` `PrimeSpectrum.instIsEmptyOfSubsingleton`
`ringKrullDim_eq_of_ringEquiv` 📖	mathematical	—	`ringKrullDim`	—	`le_antisymm` `ringKrullDim_le_of_surjective` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `RingEquiv.surjective`
`ringKrullDim_le_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim`	—	`Order.krullDim_le_of_strictMono` `RingHom.instRingHomClass` `Ideal.IsPrime.comap` `PrimeSpectrum.isPrime` `Monotone.strictMono_of_injective` `Ideal.comap_mono` `PrimeSpectrum.ext_iff` `Ideal.comap_injective_of_surjective`
`ringKrullDim_lt_top` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLT` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `Top.top` `WithBot.instTop` `instTopENat`	—	`Ne.lt_top` `ringKrullDim_ne_top`
`ringKrullDim_ne_bot` 📖	—	—	—	—	`Order.krullDim_ne_bot_of_finiteDimensionalOrder`
`ringKrullDim_ne_top` 📖	—	—	—	—	`Order.krullDim_ne_top_of_finiteDimensionalOrder`
`ringKrullDim_nonneg_of_nontrivial` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithBot.zero` `instZeroENat` `ringKrullDim`	—	`Order.krullDim_nonneg` `PrimeSpectrum.instNonemptyOfNontrivial`
`ringKrullDim_quotient_le` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.Quotient.commSemiring`	—	`ringKrullDim_le_of_surjective` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective`

---

← Back to Index