Documentation Verification Report

Zero

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

Statistics

Metric	Count
Definitions `unique_of_ringKrullDimLE_zero`	1
Theorems `jacobson_eq_radical`, `of_isMaximal_nilradical`, `subsingleton_iff_isField_of_isReduced`, `eq_maximalIdeal_of_isPrime`, `existsUnique_isPrime`, `isField_of_isDomain`, `isField_of_isReduced`, `isNilpotent_iff_mem_maximalIdeal`, `isNilpotent_iff_mem_nonunits`, `mem_minimalPrimes_iff`, `mem_minimalPrimes_iff_le_of_isPrime`, `minimalPrimes_eq_setOf_isMaximal`, `minimalPrimes_eq_setOf_isPrime`, `nilradical_eq_maximalIdeal`, `of_isLocalization`, `of_isMaximal_nilradical`, `radical_eq_maximalIdeal`, `subsingleton_primeSpectrum`, `krullDimLE_zero_and_isLocalRing_tfae`, `instIsJacobsonRingOfKrullDimLEOfNatNat`, `le_isUnit_iff_zero_notMem`, `ringKrullDimZero_iff_ringKrullDim_eq_zero`	22
Total	23

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`jacobson_eq_radical` 📖	mathematical	—	`jacobson` `CommRing.toRing` `radical` `CommRing.toCommSemiring`	—	`radical_eq_sInf`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_isMaximal_nilradical` 📖	mathematical	—	`IsLocalRing` `CommSemiring.toSemiring`	—	`List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae`

PrimeSpectrum

Definitions

Name	Category	Theorems
`unique_of_ringKrullDimLE_zero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_iff_isField_of_isReduced` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `IsField` `CommSemiring.toSemiring`	—	`Function.Injective.subsingleton` `MaximalSpectrum.toPrimeSpectrum_injective` `IsLocalRing.of_singleton_maximalSpectrum` `MaximalSpectrum.instNonemptyOfNontrivial` `Ring.KrullDimLE.isField_of_isReduced` `Order.instKrullDimLEOfNatNatOfSubsingleton` `Unique.instSubsingleton`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`krullDimLE_zero_and_isLocalRing_tfae` 📖	mathematical	—	`List.TFAE` `KrullDimLE` `IsLocalRing` `CommSemiring.toSemiring` `ExistsUnique` `Ideal` `Ideal.IsPrime` `Ideal.IsMaximal` `nilradical`	—	`nilradical.eq_1` `Ideal.radical_eq_sInf` `sInf_singleton` `Ideal.eq_top_iff_one` `IsNilpotent.zero` `isUnit_one` `one_pow` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `Ideal.eq_top_of_isUnit_mem` `Iff.not` `Ideal.IsMaximal.isPrime` `Ideal.IsMaximal.eq_of_le` `Ideal.IsPrime.ne_top` `nilradical_le_prime` `Ideal.exists_le_maximal` `KrullDimLE.mk₀` `IsLocalRing.of_unique_max_ideal` `List.tfae_of_cycle`

Ring.KrullDimLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_maximalIdeal_of_isPrime` 📖	mathematical	—	`IsLocalRing.maximalIdeal`	—	`ExistsUnique.unique` `List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal`
`existsUnique_isPrime` 📖	mathematical	—	`ExistsUnique` `Ideal` `CommSemiring.toSemiring` `Ideal.IsPrime`	—	`List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae`
`isField_of_isDomain` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring`	—	`Ring.not_isField_iff_exists_prime` `IsDomain.toNontrivial` `Ideal.IsMaximal.eq_of_le` `Ideal.IsPrime.isMaximal'` `Ideal.isPrime_bot` `IsDomain.to_noZeroDivisors` `Ideal.IsPrime.ne_top` `bot_le`
`isField_of_isReduced` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring`	—	`IsLocalRing.isField_iff_maximalIdeal_eq` `nilradical_eq_maximalIdeal` `nilradical_eq_zero` `Ideal.zero_eq_bot`
`isNilpotent_iff_mem_maximalIdeal` 📖	mathematical	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `IsLocalRing.maximalIdeal`	—	`List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae`
`isNilpotent_iff_mem_nonunits` 📖	mathematical	—	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Set` `Set.instMembership` `nonunits`	—	`isNilpotent_iff_mem_maximalIdeal`
`mem_minimalPrimes_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Ideal.minimalPrimes` `Ideal.IsPrime` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Eq.ge` `Ideal.IsMaximal.eq_of_le` `Ideal.IsPrime.isMaximal'` `Ideal.IsPrime.ne_top`
`mem_minimalPrimes_iff_le_of_isPrime` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Ideal.minimalPrimes` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`mem_minimalPrimes_iff`
`minimalPrimes_eq_setOf_isMaximal` 📖	mathematical	—	`minimalPrimes` `setOf` `Ideal` `CommSemiring.toSemiring` `Ideal.IsMaximal`	—	`Set.ext` `minimalPrimes_eq_setOf_isPrime`
`minimalPrimes_eq_setOf_isPrime` 📖	mathematical	—	`minimalPrimes` `setOf` `Ideal` `CommSemiring.toSemiring` `Ideal.IsPrime`	—	`Set.ext`
`nilradical_eq_maximalIdeal` 📖	mathematical	—	`nilradical` `IsLocalRing.maximalIdeal`	—	`Ideal.ext` `isNilpotent_iff_mem_maximalIdeal`
`of_isLocalization` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `minimalPrimes`	`Ring.KrullDimLE`	—	`IsLocalization.subsingleton_primeSpectrum_of_mem_minimalPrimes` `Order.krullDim_nonpos_of_subsingleton`
`of_isMaximal_nilradical` 📖	mathematical	—	`Ring.KrullDimLE`	—	`List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae`
`radical_eq_maximalIdeal` 📖	mathematical	—	`Ideal.radical` `IsLocalRing.maximalIdeal`	—	`Ideal.radical_eq_sInf` `LE.le.antisymm` `sInf_le` `IsLocalRing.le_maximalIdeal` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `le_sInf` `Eq.ge` `eq_maximalIdeal_of_isPrime`
`subsingleton_primeSpectrum` 📖	mathematical	—	`PrimeSpectrum`	—	`PrimeSpectrum.ext` `eq_maximalIdeal_of_isPrime` `PrimeSpectrum.isPrime`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsJacobsonRingOfKrullDimLEOfNatNat` 📖	mathematical	—	`IsJacobsonRing`	—	`Ideal.jacobson_eq_radical` `Ideal.IsRadical.radical`
`le_isUnit_iff_zero_notMem` 📖	mathematical	—	`Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.instMembership` `Submonoid.instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`List.TFAE.out` `Ring.krullDimLE_zero_and_isLocalRing_tfae` `not_isUnit_zero` `IsLocalRing.toNontrivial` `Iff.not_left` `pow_mem` `Submonoid.instSubmonoidClass`
`ringKrullDimZero_iff_ringKrullDim_eq_zero` 📖	mathematical	—	`Ring.KrullDimLE` `ringKrullDim` `WithBot` `ENat` `WithBot.zero` `instZeroENat`	—	`Ring.KrullDimLE.eq_1` `Order.krullDimLE_iff` `le_antisymm_iff` `ringKrullDim.eq_1` `Nat.cast_zero` `ringKrullDim_nonneg_of_nontrivial`

---

← Back to Index