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	RelSeries.toFun RelSeries.length RelSeries.head	—	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 AddLeftCancelSemigroup.toIsLeftCancelAdd 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	asIdeal Submodule.instPartialOrder	—	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 IsOrderedRing.toZeroLEOneClass NeZero.charZero_one ext Ideal.height_le_iff not_lt_zero le_refl
exist_mem_one_of_mem_two 📖	—	PrimeSpectrum CommRing.toCommSemiring Preorder.toLT PartialOrder.toPreorder instPartialOrder Ideal CommSemiring.toSemiring SetLike.instMembership Submodule.setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule asIdeal	—	—	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	4 math math: Order.krullDim_eq_iSup_length, Order.coheight_eq_iSup_head_eq, Order.coheight_eq, Order.height_eq_iSup_last_eq

---

← Back to Index