Documentation Verification Report

LTSeries

📁 Source: Mathlib/RingTheory/Spectrum/Prime/LTSeries.lean

Statistics

Metric	Count
Definitions `LTSeries`	1
Theorems `exist_ltSeries_mem_one_of_mem_last`, `exist_mem_one_of_mem_maximal_ideal`, `exist_mem_one_of_mem_two`	3
Total	4

PrimeSpectrum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exist_ltSeries_mem_one_of_mem_last` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal` `RelSeries.last` `PrimeSpectrum` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	`LTSeries` `PrimeSpectrum` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal` `RelSeries.toFun` `setOf` `Preorder.toLT` `RelSeries.length` `RelSeries.head` `RelSeries.last`	—	`RelSeries.last_singleton` `RelSeries.last.eq_1` `zero_add` `exist_mem_one_of_mem_two` `LTSeries.strictMono` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `tsub_zero` `RelSeries.last_snoc` `Eq.trans_ne` `Fin.one_eq_mk_of_lt` `RelSeries.snoc_castSucc` `RelSeries.head_snoc`
`exist_mem_one_of_mem_maximal_ideal` 📖	mathematical	`PrimeSpectrum` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `IsLocalRing.closedPoint` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal`	`PrimeSpectrum` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `IsLocalRing.maximalIdeal`	—	`LT.lt.le` `Ideal.nonempty_minimalPrimes` `LT.lt.ne` `LE.le.trans_lt` `sup_le` `IsLocalRing.le_maximalIdeal_of_isPrime` `isPrime` `Ideal.span_singleton_le_iff_mem` `Ne.lt_top` `Ideal.IsPrime.ne_top'` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `LE.le.trans` `le_sup_right` `Ideal.mem_span_singleton_self` `lt_of_le_not_ge` `le_sup_left` `lt_of_le_of_ne` `Ideal.map_height_le_one_of_mem_minimalPrimes` `Order.lt_one_iff_nonpos` `NeZero.charZero_one` `ext` `Ideal.height_le_iff` `not_lt_zero` `le_refl`
`exist_mem_one_of_mem_two` 📖	mathematical	`PrimeSpectrum` `CommRing.toCommSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal`	`PrimeSpectrum` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `asIdeal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	—	`isPrime` `Localization.isLocalization` `Localization.AtPrime.isLocalRing` `le_refl` `ext` `Localization.AtPrime.map_eq_maximalIdeal` `LT.lt.le` `LT.lt.trans` `exist_mem_one_of_mem_maximal_ideal` `IsLocalization.instIsNoetherianRingLocalization` `OrderIso.lt_iff_lt` `Ideal.mem_map_of_mem` `LT.lt.trans_eq` `OrderIso.symm_apply_apply` `Eq.le` `Ideal.under_map_of_isLocalizationAtPrime`

(root)

Definitions

Name	Category	Theorems
`LTSeries` 📖	CompOp	15 math math: `Order.exists_series_of_le_height`, `Order.le_krullDim_iff`, `Ideal.exists_ltSeries_length_eq_height`, `Order.krullDim_eq_iSup_length`, `Order.coheight_eq_iSup_head_eq`, `PrimeSpectrum.exist_ltSeries_mem_one_of_mem_last`, `Order.exists_series_of_coheight_eq_coe`, `Ideal.exists_ltSeries_of_hasGoingDown`, `Order.coheight_eq_top_iff`, `Order.exists_series_of_le_coheight`, `Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support`, `Order.exists_series_of_height_eq_coe`, `Order.coheight_eq`, `Order.height_eq_iSup_last_eq`, `Order.height_eq_top_iff`

---

← Back to Index