Height

📁 Source: Mathlib/RingTheory/Ideal/Height.lean

Statistics

Metric	Count
Definitions `FiniteHeight`, `height`, `primeHeight`	3
Theorems `eq_top_or_height_ne_top`, `exists_isMaximal_height`, `exists_ltSeries_length_eq_height`, `finiteHeight_iff`, `finiteHeight_iff_lt`, `finiteHeight_of_finiteRingKrullDim`, `finiteHeight_of_le`, `height_bot`, `height_eq_primeHeight`, `height_le_iff`, `height_le_iff_covBy`, `height_le_ringKrullDim_of_ne_top`, `height_lt_top`, `height_mono`, `height_ne_top`, `height_of_subsingleton`, `height_strict_mono_of_is_prime`, `height_top`, `isMaximal_of_primeHeight_eq_ringKrullDim`, `mem_minimalPrimes_of_height_eq`, `primeHeight_add_one_le_of_lt`, `primeHeight_eq_ringKrullDim_iff`, `primeHeight_eq_zero_iff`, `primeHeight_le_ringKrullDim`, `primeHeight_lt_top`, `primeHeight_mono`, `primeHeight_ne_top`, `primeHeight_strict_mono`, `sup_height_eq_ringKrullDim`, `sup_primeHeight_eq_ringKrullDim`, `sup_primeHeight_of_maximal_eq_ringKrullDim`, `maximalIdeal_height_eq_ringKrullDim`, `maximalIdeal_primeHeight_eq_ringKrullDim`, `ringKrullDim_eq_height`, `height_comap`, `height_map_of_disjoint`, `primeHeight_comap`, `krullDimLE_of_isLocalization_maximal`, `height_comap`, `height_map`, `exists_spanRank_le_and_le_height_of_le_height`, `mem_minimalPrimes_of_primeHeight_eq_height`, `ringKrullDim_le_iff_height_le`, `ringKrullDim_le_iff_isMaximal_height_le`	44
Total	47

Ideal

Definitions

Name	Category	Theorems
`FiniteHeight` 📖	CompData	5 math math: `finiteHeight_of_le`, `finiteHeight_of_isNoetherianRing`, `finiteHeight_iff`, `finiteHeight_iff_lt`, `finiteHeight_of_finiteRingKrullDim`
`height` 📖	CompOp	45 math math: `height_le_spanFinrank`, `height_le_spanRank`, `height_le_iff_exists_minimalPrimes`, `height_of_subsingleton`, `height_top`, `height_lt_top`, `exists_finset_card_eq_height_of_isNoetherianRing`, `height_eq_height_add_of_liesOver_of_hasGoingDown`, `height_strict_mono_of_is_prime`, `Polynomial.height_eq_height_add_one`, `exists_ltSeries_length_eq_height`, `IsPrincipalIdealRing.height_eq_one_of_isMaximal`, `height_le_height_add_of_liesOver`, `height_le_height_add_one_of_mem`, `Polynomial.height_map_C`, `height_le_card_of_mem_minimalPrimes_span`, `exists_isMaximal_height`, `height_le_spanRank_toENat_of_mem_minimal_primes`, `IsLocalization.height_map_of_disjoint`, `ringKrullDim_le_iff_height_le`, `height_mono`, `height_eq_primeHeight`, `height_le_ringKrullDim_quotient_add_one`, `height_le_iff`, `IsLocalization.AtPrime.ringKrullDim_eq_height`, `height_le_ringKrullDim_quotient_add_encard`, `RingEquiv.height_comap`, `height_le_iff_covBy`, `ringKrullDim_le_iff_isMaximal_height_le`, `RingEquiv.height_map`, `map_height_le_one_of_mem_minimalPrimes`, `sup_height_eq_ringKrullDim`, `finiteHeight_iff_lt`, `height_le_ringKrullDim_quotient_add_spanFinrank`, `height_le_height_add_encard_of_subset`, `height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing`, `IsLocalRing.maximalIdeal_height_eq_ringKrullDim`, `height_le_one_of_isPrincipal_of_mem_minimalPrimes`, `exists_spanRank_eq_and_height_eq`, `height_le_height_add_spanFinrank_of_le`, `height_le_spanRank_toENat`, `height_le_card_of_mem_minimalPrimes_span_finset`, `height_le_ringKrullDim_of_ne_top`, `height_bot`, `IsLocalization.height_comap`
`primeHeight` 📖	CompOp	12 math math: `sup_primeHeight_eq_ringKrullDim`, `primeHeight_mono`, `primeHeight_lt_top`, `primeHeight_eq_ringKrullDim_iff`, `primeHeight_le_ringKrullDim`, `sup_primeHeight_of_maximal_eq_ringKrullDim`, `primeHeight_strict_mono`, `height_eq_primeHeight`, `primeHeight_add_one_le_of_lt`, `primeHeight_eq_zero_iff`, `IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim`, `IsLocalization.primeHeight_comap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isMaximal_height` 📖	mathematical	—	`IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot.some` `ENat` `height` `ringKrullDim`	—	`exists_le_maximal` `IsPrime.ne_top'` `PrimeSpectrum.isPrime` `le_antisymm` `height_le_ringKrullDim_of_ne_top` `IsMaximal.isPrime'` `height_eq_primeHeight` `Eq.le` `LTSeries.height_last_longestOf` `height_mono`
`exists_ltSeries_length_eq_height` 📖	mathematical	—	`RelSeries.last` `PrimeSpectrum` `CommRing.toCommSemiring` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `PrimeSpectrum.instPartialOrder` `IsPrime` `CommSemiring.toSemiring` `ENat` `ENat.instNatCast` `RelSeries.length` `height`	—	`height_ne_top` `IsPrime.ne_top` `height_eq_primeHeight` `primeHeight.eq_1` `Order.exists_series_of_height_eq_coe` `WithTop.some_eq_coe` `ENat.some_eq_coe`
`finiteHeight_iff` 📖	mathematical	—	`FiniteHeight` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`finiteHeight_iff_lt` 📖	mathematical	—	`FiniteHeight` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height` `instTopENat`	—	`finiteHeight_iff` `lt_top_iff_ne_top`
`finiteHeight_of_finiteRingKrullDim` 📖	mathematical	—	`FiniteHeight`	—	`finiteHeight_iff` `lt_top_iff_ne_top` `WithBot.coe_lt_coe` `ringKrullDim_lt_top` `height_le_ringKrullDim_of_ne_top` `lt_of_le_of_lt`
`finiteHeight_of_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`FiniteHeight`	—	`lt_top_iff_ne_top` `LE.le.trans_lt` `height_mono` `height_lt_top`
`height_bot` 📖	mathematical	—	`height` `Bot.bot` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ENat` `instZeroENat`	—	`nonempty_minimalPrimes` `top_ne_bot` `instNontrivial` `primeHeight_eq_zero_iff`
`height_eq_primeHeight` 📖	mathematical	—	`height` `primeHeight`	—	`minimalPrimes_eq_subsingleton_self` `iInf_congr_Prop` `iInf_iInf_eq_left`
`height_le_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height` `ENat.instNatCast` `Preorder.toLT`	—	`height_eq_primeHeight` `primeHeight.eq_1` `Order.height_le_coe_iff` `Equiv.forall_congr_left`
`height_le_iff_covBy` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height` `ENat.instNatCast` `Preorder.toLT`	—	`height_le_iff` `exists_le_covBy_of_lt` `instIsStronglyCoatomicOfWellFoundedGT` `Subtype.wellFoundedGT` `wellFoundedGT` `LE.le.trans_lt` `height_mono`
`height_le_ringKrullDim_of_ne_top` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithBot.some` `height` `ringKrullDim` `CommRing.toCommSemiring`	—	`height.eq_1` `nonempty_minimalPrimes` `minimalPrimes_isPrime` `le_trans` `iInf₂_le` `primeHeight_le_ringKrullDim`
`height_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height` `Top.top` `instTopENat`	—	`Ne.lt_top` `height_ne_top`
`height_mono` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`ENat` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height`	—	`le_iInf₂` `minimalPrimes_isPrime` `exists_minimalPrimes_le` `LE.le.trans` `iInf₂_le` `primeHeight_mono`
`height_ne_top` 📖	—	—	—	—	`FiniteHeight.eq_top_or_height_ne_top`
`height_of_subsingleton` 📖	mathematical	—	`height` `Top.top` `ENat` `instTopENat`	—	`Unique.instSubsingleton` `height_top`
`height_strict_mono_of_is_prime` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`ENat` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height`	—	`height_eq_primeHeight` `height_top` `primeHeight_lt_top` `ENat.add_one_le_iff` `primeHeight_ne_top` `height.eq_1` `le_iInf₂` `lt_of_lt_of_le` `primeHeight_add_one_le_of_lt`
`height_top` 📖	mathematical	—	`height` `Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ENat` `instTopENat`	—	`minimalPrimes_top` `iInf_congr_Prop` `iInf_neg` `iInf_top`
`isMaximal_of_primeHeight_eq_ringKrullDim` 📖	mathematical	`WithBot.some` `ENat` `primeHeight` `ringKrullDim` `CommRing.toCommSemiring`	`IsMaximal` `CommSemiring.toSemiring`	—	`ringKrullDim_ne_top` `primeHeight.congr_simp` `height_top` `exists_le_maximal` `lt_or_eq_of_le` `IsMaximal.isPrime'` `primeHeight_strict_mono` `finiteHeight_of_finiteRingKrullDim` `primeHeight_le_ringKrullDim`
`mem_minimalPrimes_of_height_eq` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ENat` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `height`	`Set` `Set.instMembership` `minimalPrimes`	—	`exists_minimalPrimes_le` `eq_of_le_of_not_lt` `finiteHeight_of_le` `IsPrime.ne_top'` `lt_irrefl` `LT.lt.trans_le` `height_strict_mono_of_is_prime` `LE.le.trans` `height_mono`
`primeHeight_add_one_le_of_lt` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`ENat` `Preorder.toLE` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `instCommSemiringENat` `primeHeight` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Order.height_add_one_le`
`primeHeight_eq_ringKrullDim_iff` 📖	mathematical	—	`WithBot.some` `ENat` `primeHeight` `ringKrullDim` `CommRing.toCommSemiring` `IsLocalRing.maximalIdeal`	—	`IsLocalRing.eq_maximalIdeal` `isMaximal_of_primeHeight_eq_ringKrullDim` `IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim`
`primeHeight_eq_zero_iff` 📖	mathematical	—	`primeHeight` `ENat` `instZeroENat` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `minimalPrimes`	—	`primeHeight.eq_1` `Order.height_eq_zero` `minimalPrimes.eq_1` `minimalPrimes.eq_1` `Mathlib.Tactic.Push.not_forall_eq` `PrimeSpectrum.isPrime`
`primeHeight_le_ringKrullDim` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `WithBot.some` `primeHeight` `ringKrullDim` `CommRing.toCommSemiring`	—	`Order.height_le_krullDim`
`primeHeight_lt_top` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `primeHeight` `Top.top` `instTopENat`	—	`height_eq_primeHeight` `height_lt_top` `IsPrime.ne_top`
`primeHeight_mono` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`ENat` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `primeHeight`	—	`Order.height_mono`
`primeHeight_ne_top` 📖	—	—	—	—	`height_eq_primeHeight` `height_ne_top` `IsPrime.ne_top`
`primeHeight_strict_mono` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`ENat` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `primeHeight`	—	`primeHeight.eq_1` `finiteHeight_iff` `lt_top_iff_ne_top` `height_eq_primeHeight` `lt_of_le_of_lt` `primeHeight_mono` `LT.lt.le` `primeHeight_lt_top` `Order.height_strictMono`
`sup_height_eq_ringKrullDim` 📖	mathematical	—	`WithBot.some` `ENat` `iSup` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Top.top` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `height` `ringKrullDim`	—	`le_antisymm` `WithBot.coe_iSup` `le_top` `iSup_le` `iSup_congr_Prop` `height_top` `iSup_neg` `bot_eq_zero'` `iSup_pos` `WithBot.coe_le_coe` `le_trans` `PrimeSpectrum.isPrime` `height_eq_primeHeight` `le_iSup` `le_rfl` `le_iSup_of_le` `IsPrime.ne_top'`
`sup_primeHeight_eq_ringKrullDim` 📖	mathematical	—	`WithBot.some` `ENat` `iSup` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `IsPrime` `primeHeight` `ringKrullDim`	—	`sup_height_eq_ringKrullDim` `le_antisymm` `iSup_mono` `iSup_mono'` `IsPrime.ne_top` `height_eq_primeHeight` `le_refl` `iSup_congr_Prop` `height_top` `iSup_neg` `bot_eq_zero'` `Set.nonempty_coe_sort` `nonempty_minimalPrimes` `le_iSup_of_le` `iInf_le_of_le` `le_rfl` `iSup_pos`
`sup_primeHeight_of_maximal_eq_ringKrullDim` 📖	mathematical	—	`WithBot.some` `ENat` `iSup` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `IsMaximal` `primeHeight` `IsMaximal.isPrime'` `ringKrullDim`	—	`IsMaximal.isPrime'` `sup_primeHeight_eq_ringKrullDim` `le_antisymm` `iSup_mono` `iSup_mono'` `IsMaximal.isPrime` `le_rfl` `eq_or_ne` `exists_le_maximal` `primeHeight_mono`

Ideal.FiniteHeight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_top_or_height_ne_top` 📖	mathematical	—	`Top.top` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`maximalIdeal_height_eq_ringKrullDim` 📖	mathematical	—	`WithBot.some` `ENat` `Ideal.height` `maximalIdeal` `CommRing.toCommSemiring` `ringKrullDim`	—	`Ideal.IsMaximal.isPrime'` `maximalIdeal.isMaximal` `Ideal.height_eq_primeHeight` `maximalIdeal_primeHeight_eq_ringKrullDim`
`maximalIdeal_primeHeight_eq_ringKrullDim` 📖	mathematical	—	`WithBot.some` `ENat` `Ideal.primeHeight` `maximalIdeal` `CommRing.toCommSemiring` `Ideal.IsMaximal.isPrime'` `maximalIdeal.isMaximal` `ringKrullDim`	—	`Ideal.IsMaximal.isPrime'` `maximalIdeal.isMaximal` `ringKrullDim.eq_1` `Ideal.primeHeight.eq_1` `Order.height_top_eq_krullDim`

IsLocalization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`height_comap` 📖	mathematical	—	`Ideal.height` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `Ideal.height.eq_1` `Ideal.IsPrime.under` `iInf_congr_Prop` `primeHeight_comap` `minimalPrimes_comap` `iInf_image`
`height_map_of_disjoint` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submonoid.instSetLike` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Ideal.height` `Ideal.map` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`isPrime_of_isPrime_disjoint` `RingHom.instRingHomClass` `Ideal.IsPrime.under` `isLocalization_isLocalization_atPrime_isLocalization` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization` `ringKrullDim_eq_of_ringEquiv` `comap_map_of_isPrime_disjoint` `AtPrime.congr_simp` `WithBot.coe_eq_coe` `AtPrime.ringKrullDim_eq_height`
`primeHeight_comap` 📖	mathematical	—	`Ideal.primeHeight` `Ideal.comap` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `RingHom.instRingHomClass` `Ideal.IsPrime.under`	—	`RingHom.instRingHomClass` `Ideal.IsPrime.under` `Ideal.primeHeight.eq_1` `Order.height_eq_krullDim_Iic` `Set.disjoint_of_subset_right` `Order.krullDim_eq_of_orderIso` `PrimeSpectrum.isPrime` `Ideal.comap_mono` `Ideal.map_le_iff_le_comap` `PrimeSpectrum.ext_iff` `Equiv.left_inv` `Equiv.right_inv` `RelIso.map_rel_iff`

IsLocalization.AtPrime

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ringKrullDim_eq_height` 📖	mathematical	—	`ringKrullDim` `CommRing.toCommSemiring` `WithBot.some` `ENat` `Ideal.height`	—	`isLocalRing` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `IsLocalRing.maximalIdeal_primeHeight_eq_ringKrullDim` `RingHom.instRingHomClass` `Ideal.IsPrime.under` `IsLocalization.primeHeight_comap` `comap_maximalIdeal` `Ideal.height_eq_primeHeight`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`krullDimLE_of_isLocalization_maximal` 📖	—	`IsLocalization.AtPrime` `CommRing.toCommSemiring` `Ideal.IsMaximal.isPrime'` `KrullDimLE`	—	—	`Ideal.IsMaximal.isPrime'` `Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `ringKrullDim_eq_bot_of_subsingleton` `Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim` `WithBot.coe_le_coe` `iSup₂_le_iff` `Ideal.height_eq_primeHeight` `IsLocalization.AtPrime.ringKrullDim_eq_height`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`height_comap` 📖	mathematical	—	`Ideal.height` `Ideal.comap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `instEquivLike` `RingEquivClass.toRingHomClass` `Semiring.toNonAssocSemiring` `instRingEquivClass`	—	`RingEquivClass.toRingHomClass` `instRingEquivClass` `Equiv.iInf_congr` `RingHom.instRingHomClass` `Ideal.comap_coe` `Ideal.comap_minimalPrimes_eq_of_surjective` `surjective` `Function.Injective.mem_set_image` `OrderIso.injective`
`height_map` 📖	mathematical	—	`Ideal.height` `Ideal.map` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Distrib.toAdd` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EquivLike.toFunLike` `instEquivLike`	—	`RingEquivClass.toRingHomClass` `instRingEquivClass` `Ideal.comap_symm` `height_comap`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_spanRank_le_and_le_height_of_le_height` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `Ideal.height`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Cardinal` `Cardinal.instLE` `Submodule.spanRank` `Cardinal.instNatCast`	—	`bot_le` `Submodule.spanRank_bot` `le_refl` `zero_le` `LE.le.trans` `WithTop.coe_le_coe` `Set.Finite.subset` `Ideal.finite_minimalPrimes_of_isNoetherianRing` `Iff.not` `Ideal.subset_union_prime` `Set.Finite.mem_toFinset` `Mathlib.Tactic.Push.not_and_eq` `Ideal.height_mono` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `not_lt` `sup_le` `Ideal.span_le` `Set.singleton_subset_iff` `Submodule.spanRank_sup_le_sum_spanRank` `Nat.cast_add` `Nat.cast_one` `add_le_add` `Cardinal.addLeftMono` `Cardinal.addRightMono` `Submodule.spanRank_span_le_card` `Cardinal.mk_fintype` `Fintype.card_unique` `le_iInf₂` `Ideal.height_eq_primeHeight` `le_top` `le_sup_left` `le_antisymm` `mem_minimalPrimes_of_primeHeight_eq_height` `Ideal.mem_sup_right` `Ideal.subset_span` `Set.mem_singleton` `Order.add_one_le_of_lt` `lt_of_le_of_ne`
`mem_minimalPrimes_of_primeHeight_eq_height` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.primeHeight` `Ideal.height`	`Set` `Set.instMembership` `Ideal.minimalPrimes`	—	`Ideal.mem_minimalPrimes_of_height_eq` `le_refl` `Ideal.height_eq_primeHeight`
`ringKrullDim_le_iff_height_le` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `CommRing.toCommSemiring` `WithBot.some` `Ideal.height`	—	`ringKrullDim.eq_1` `Order.krullDim_eq_iSup_height` `iSup_le_iff` `Ideal.height_eq_primeHeight` `PrimeSpectrum.isPrime`
`ringKrullDim_le_iff_isMaximal_height_le` 📖	mathematical	—	`WithBot` `ENat` `Preorder.toLE` `WithBot.instPreorder` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ringKrullDim` `CommRing.toCommSemiring` `WithBot.some` `Ideal.height`	—	`ringKrullDim_le_iff_height_le` `Ideal.IsMaximal.isPrime` `Ideal.exists_le_maximal` `Ideal.IsPrime.ne_top` `le_trans` `Ideal.height_mono`

---

← Back to Index