Documentation Verification Report

Module

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

Statistics

Metric	Count
Definitions `supportDim`	1
Theorems `supportDim_eq_bot_iff_subsingleton`, `supportDim_eq_bot_of_subsingleton`, `supportDim_eq_of_equiv`, `supportDim_eq_ringKrullDim_quotient_annihilator`, `supportDim_le_of_injective`, `supportDim_le_of_surjective`, `supportDim_le_ringKrullDim`, `supportDim_ne_bot_iff_nontrivial`, `supportDim_ne_bot_of_nontrivial`, `supportDim_quotient_eq_ringKrullDim`, `supportDim_self_eq_ringKrullDim`, `support_of_supportDim_eq_zero`	12
Total	13

Module

Definitions

Name	Category	Theorems
`supportDim` 📖	CompOp	17 math math: `supportDim_eq_bot_iff_subsingleton`, `supportDim_eq_ringKrullDim_quotient_annihilator`, `supportDim_add_length_eq_supportDim_of_isRegular`, `supportDim_self_eq_ringKrullDim`, `supportDim_le_of_injective`, `supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal`, `supportDim_quotSMulTop_succ_eq_supportDim`, `supportDim_le_ringKrullDim`, `supportDim_le_supportDim_quotSMulTop_succ`, `supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson`, `supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson`, `supportDim_eq_of_equiv`, `supportDim_quotient_eq_ringKrullDim`, `supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson`, `supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes`, `supportDim_le_of_surjective`, `supportDim_eq_bot_of_subsingleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`supportDim_eq_bot_iff_subsingleton` 📖	mathematical	—	`supportDim` `Bot.bot` `WithBot` `ENat` `WithBot.bot`	—	—
`supportDim_eq_bot_of_subsingleton` 📖	mathematical	—	`supportDim` `Bot.bot` `WithBot` `ENat` `WithBot.bot`	—	—
`supportDim_eq_of_equiv` 📖	mathematical	—	`supportDim`	—	`RingHomInvPair.ids` `le_antisymm` `supportDim_le_of_injective` `LinearEquiv.injective` `supportDim_le_of_surjective` `LinearEquiv.surjective`
`supportDim_eq_ringKrullDim_quotient_annihilator` 📖	mathematical	—	`supportDim` `ringKrullDim` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `annihilator` `AddCommGroup.toAddCommMonoid` `Ideal.Quotient.commSemiring`	—	`support_eq_zeroLocus` `ringKrullDim_quotient`
`supportDim_le_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `supportDim`	—	`Order.krullDim_le_of_strictMono` `support_subset_of_injective`
`supportDim_le_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `supportDim`	—	`Order.krullDim_le_of_strictMono` `support_subset_of_surjective`
`supportDim_le_ringKrullDim` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `supportDim` `ringKrullDim` `CommRing.toCommSemiring`	—	`Order.krullDim_le_of_strictMono`
`supportDim_ne_bot_iff_nontrivial` 📖	mathematical	—	`Nontrivial`	—	—
`supportDim_ne_bot_of_nontrivial` 📖	—	—	—	—	`Set.Nonempty.to_subtype` `nonempty_support_of_nontrivial`
`supportDim_quotient_eq_ringKrullDim` 📖	mathematical	—	`supportDim` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Submodule.Quotient.addCommGroup` `CommRing.toRing` `Ring.toAddCommGroup` `Semiring.toModule` `Submodule.Quotient.module` `ringKrullDim` `Ideal.Quotient.commSemiring`	—	`supportDim_eq_ringKrullDim_quotient_annihilator` `Finite.quotient` `Finite.self` `Ideal.annihilator_quotient` `Ideal.instIsTwoSided_1`
`supportDim_self_eq_ringKrullDim` 📖	mathematical	—	`supportDim` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ringKrullDim`	—	`annihilator_eq_bot` `faithfulSMul_iff_algebraMap_injective` `supportDim_eq_ringKrullDim_quotient_annihilator` `Finite.self` `RingEquiv.ringKrullDim`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`support_of_supportDim_eq_zero` 📖	mathematical	`Module.supportDim` `WithBot` `ENat` `WithBot.zero` `instZeroENat`	`Module.support` `PrimeSpectrum.zeroLocus` `CommRing.toCommSemiring` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal`	—	`Module.supportDim_ne_bot_iff_nontrivial` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `PrimeSpectrum.zeroLocus_eq_singleton` `le_antisymm` `lt_of_le_of_ne` `IsLocalRing.le_maximalIdeal` `Ideal.IsPrime.ne_top'` `PrimeSpectrum.isPrime` `IsLocalRing.closedPoint_mem_support` `ne_of_lt`

---

← Back to Index