KrullDimension

📁 Source: Mathlib/Order/KrullDimension.lean

Statistics

Metric	Count
Definitions KrullDimLE, coheight, height, krullDim	4
Theorems height_last_longestOf, coheight_eq_zero, height_eq_zero, krullDim_le, mono, length_le_krullDim, bot_lt_krullDim, bot_lt_krullDim_iff, coe_lt_coheight_iff, coe_lt_height_iff, coheight_add_one_le, coheight_anti, coheight_bot_eq_krullDim, coheight_coe_enat, coheight_coe_withBot, coheight_coe_withTop, coheight_eq, coheight_eq_coe_add_one_iff, coheight_eq_coe_iff, coheight_eq_coe_iff_maximal_le_coheight, coheight_eq_iSup_gt_coheight, coheight_eq_iSup_head_eq, coheight_eq_index_of_length_eq_head_coheight, coheight_eq_krullDim_Ici, coheight_eq_top_iff, coheight_eq_zero, coheight_int, coheight_le, coheight_le_coe_iff, coheight_le_coheight_apply_of_strictMono, coheight_le_iff, coheight_le_iff', coheight_le_krullDim, coheight_le_of_krullDim_preimage_le, coheight_nat, coheight_ne_zero, coheight_ofDual, coheight_of_noMaxOrder, coheight_orderIso, coheight_pos, coheight_pos_of_lt_top, coheight_strictAnti, coheight_toDual, coheight_top, exists_series_of_coheight_eq_coe, exists_series_of_height_eq_coe, exists_series_of_le_coheight, exists_series_of_le_height, finiteDimensionalOrder_iff_krullDim_ne_bot_and_top, height_add_one_le, height_bot, height_coe_withBot, height_coe_withTop, height_enat, height_eq_coe_add_one_iff, height_eq_coe_iff, height_eq_coe_iff_minimal_le_height, height_eq_iSup_last_eq, height_eq_iSup_lt_height, height_eq_index_of_length_eq_height_last, height_eq_krullDim_Iic, height_eq_top_iff, height_eq_zero, height_int, height_le, height_le_coe_iff, height_le_height_apply_of_strictMono, height_le_iff, height_le_iff', height_le_krullDim, height_le_of_krullDim_preimage_le, height_mono, height_nat, height_ne_zero, height_ofDual, height_of_noMinOrder, height_orderIso, height_pos, height_pos_of_bot_lt, height_strictMono, height_toDual, height_top_eq_krullDim, index_le_height, instKrullDimLEOfNatNatOfSubsingleton, krullDimLE_iff, krullDim_WithTop, krullDim_enat, krullDim_eq_bot, krullDim_eq_bot_iff, krullDim_eq_iSup_coheight, krullDim_eq_iSup_coheight_of_nonempty, krullDim_eq_iSup_height, krullDim_eq_iSup_height_add_coheight_of_nonempty, krullDim_eq_iSup_height_of_nonempty, krullDim_eq_iSup_length, krullDim_eq_length_of_finiteDimensionalOrder, krullDim_eq_of_orderIso, krullDim_eq_one_iff_of_boundedOrder, krullDim_eq_top, krullDim_eq_top_iff, krullDim_eq_zero, krullDim_eq_zero_iff_of_orderBot, krullDim_eq_zero_iff_of_orderTop, krullDim_eq_zero_of_unique, krullDim_int, krullDim_le_of_krullDim_preimage_le, krullDim_le_of_krullDim_preimage_le', krullDim_le_of_strictComono_and_surj, krullDim_le_of_strictMono, krullDim_le_one_iff, krullDim_le_one_iff_forall_isMax, krullDim_le_one_iff_forall_isMin, krullDim_le_one_iff_of_boundedOrder, krullDim_lt_coe_iff, krullDim_nat, krullDim_ne_bot_iff, krullDim_ne_bot_of_finiteDimensionalOrder, krullDim_ne_top_of_finiteDimensionalOrder, krullDim_nonneg, krullDim_nonneg_iff, krullDim_nonpos_iff_forall_isMax, krullDim_nonpos_iff_forall_isMin, krullDim_nonpos_of_subsingleton, krullDim_of_isSimpleOrder, krullDim_of_noMaxOrder, krullDim_of_noMinOrder, krullDim_orderDual, krullDim_pos_iff, krullDim_pos_iff_of_orderBot, krullDim_pos_iff_of_orderTop, krullDim_withBot, le_krullDim_iff, length_le_coheight, length_le_coheight_head, length_le_height, length_le_height_last, one_le_krullDim_iff, one_lt_height_iff, rev_index_le_coheight	139
Total	143

LTSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_last_longestOf 📖	mathematical	—	WithBot.some ENat Order.height RelSeries.last setOf Preorder.toLT longestOf Order.krullDim	—	le_antisymm Order.height_le_krullDim Order.krullDim_eq_length_of_finiteDimensionalOrder Order.height.eq_1 le_iSup_iff iSup_le_iff le_rfl

Order

Definitions

Name	Category	Theorems
KrullDimLE 📖	CompData	3 math math: KrullDimLE.mono, instKrullDimLEOfNatNatOfSubsingleton, krullDimLE_iff
coheight 📖	CompOp	45 math math: coheight_add_one_le, height_ofDual, coheight_le, length_le_coheight, coheight_le_krullDim, coheight_eq_coe_add_one_iff, krullDim_eq_iSup_coheight_of_nonempty, coheight_pos_of_lt_top, coheight_eq_coe_iff_maximal_le_coheight, IsMax.coheight_eq_zero, coheight_eq_iSup_head_eq, coheight_int, coheight_coe_withTop, coheight_of_noMaxOrder, coheight_eq_krullDim_Ici, coheight_le_of_krullDim_preimage_le, krullDim_eq_iSup_coheight, coheight_eq_zero, coheight_top, coheight_eq_top_iff, coheight_le_coheight_apply_of_strictMono, coheight_le_iff', coheight_eq_index_of_length_eq_head_coheight, coe_lt_coheight_iff, coheight_nat, coheight_le_coe_iff, Module.length_eq_coheight, coheight_coe_enat, krullDim_eq_iSup_height_add_coheight_of_nonempty, coheight_coe_withBot, coheight_eq_coe_iff, coheight_bot_eq_krullDim, Module.length_quotient, coheight_anti, coheight_pos, coheight_eq, rev_index_le_coheight, coheight_eq_iSup_gt_coheight, length_le_coheight_head, coheight_ofDual, coheight_orderIso, height_toDual, coheight_le_iff, coheight_toDual, coheight_strictAnti
height 📖	CompOp	49 math math: AlgebraicGeometry.Scheme.height_of_isClosed, height_ofDual, height_add_one_le, height_nat, height_pos, height_orderIso, Submodule.height_strictMono, height_le_krullDim, height_coe_withTop, height_pos_of_bot_lt, height_eq_zero, height_of_noMinOrder, Module.length_submodule, krullDim_eq_iSup_height_of_nonempty, height_strictMono, height_eq_iSup_lt_height, height_eq_coe_add_one_iff, height_le_coe_iff, height_eq_coe_iff, height_eq_krullDim_Iic, length_le_height, height_le_height_apply_of_strictMono, height_le_of_krullDim_preimage_le, krullDim_eq_iSup_height, height_le, height_top_eq_krullDim, height_bot, krullDim_eq_iSup_height_add_coheight_of_nonempty, height_int, height_le_iff, Module.length_eq_height, IsMin.height_eq_zero, height_mono, height_le_iff', LTSeries.height_last_longestOf, index_le_height, height_coe_withBot, height_eq_iSup_last_eq, height_enat, length_le_height_last, coe_lt_height_iff, Submodule.height_lt_top, height_eq_top_iff, coheight_ofDual, height_eq_coe_iff_minimal_le_height, height_toDual, one_lt_height_iff, coheight_toDual, height_eq_index_of_length_eq_height_last
krullDim 📖	CompOp	59 math math: LTSeries.length_le_krullDim, krullDim_le_of_strictComono_and_surj, krullDim_of_noMaxOrder, krullDim_lt_coe_iff, krullDim_nonneg_iff, krullDim_pos_iff, krullDim_le_one_iff, ringKrullDim_quotient, krullDim_eq_zero_of_unique, le_krullDim_iff, krullDim_eq_top, coheight_le_krullDim, krullDim_nonpos_iff_forall_isMax, krullDim_nonpos_iff_forall_isMin, krullDim_int, krullDim_le_of_krullDim_preimage_le, height_le_krullDim, Module.coe_length, bot_lt_krullDim, krullDim_eq_iSup_coheight_of_nonempty, krullDim_eq_iSup_length, krullDim_nonpos_of_subsingleton, krullDim_eq_of_orderIso, krullDim_WithTop, krullDim_eq_iSup_height_of_nonempty, coheight_eq_krullDim_Ici, krullDim_enat, height_eq_krullDim_Iic, krullDim_le_one_iff_of_boundedOrder, krullDim_eq_iSup_coheight, krullDim_eq_bot_iff, krullDim_eq_iSup_height, height_top_eq_krullDim, krullDim_eq_zero_iff_of_orderTop, one_le_krullDim_iff, krullDim_le_of_strictMono, krullDim_orderDual, krullDim_le_one_iff_forall_isMax, krullDim_withBot, krullDim_pos_iff_of_orderTop, krullDim_eq_zero, krullDim_eq_iSup_height_add_coheight_of_nonempty, krullDim_pos_iff_of_orderBot, krullDim_eq_bot, coheight_bot_eq_krullDim, krullDim_eq_length_of_finiteDimensionalOrder, KrullDimLE.krullDim_le, krullDim_eq_one_iff_of_boundedOrder, krullDim_nonneg, LTSeries.height_last_longestOf, krullDim_le_one_iff_forall_isMin, krullDim_of_noMinOrder, krullDim_of_isSimpleOrder, krullDim_eq_zero_iff_of_orderBot, bot_lt_krullDim_iff, krullDim_le_of_krullDim_preimage_le', krullDim_nat, krullDimLE_iff, krullDim_eq_top_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_lt_krullDim 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat Bot.bot WithBot.bot krullDim	—	bot_lt_krullDim_iff
bot_lt_krullDim_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat Bot.bot WithBot.bot krullDim	—	bot_lt_iff_ne_bot krullDim_ne_bot_iff
coe_lt_coheight_iff 📖	mathematical	ENat instLTENat coheight Top.top instTopENat	ENat instLTENat ENat.instNatCast coheight Preorder.toLT	—	coe_lt_height_iff
coe_lt_height_iff 📖	mathematical	ENat instLTENat height Top.top instTopENat	ENat instLTENat ENat.instNatCast height Preorder.toLT	—	LT.lt.ne_top exists_series_of_height_eq_coe IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid LTSeries.strictMono height_eq_index_of_length_eq_height_last height_strictMono lt_of_le_of_lt height_mono LT.lt.le
coheight_add_one_le 📖	mathematical	Preorder.toLT	ENat instLEENat instAddENat coheight AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	coheight_anti le_of_lt top_add add_one_le_of_lt coheight_strictAnti
coheight_anti 📖	mathematical	—	Antitone ENat instPreorderENat coheight	—	Monotone.dual_left height_mono
coheight_bot_eq_krullDim 📖	mathematical	—	WithBot.some ENat coheight Bot.bot OrderBot.toBot Preorder.toLE krullDim	—	krullDim_orderDual height_top_eq_krullDim
coheight_coe_enat 📖	mathematical	—	coheight ENat instPreorderENat ENat.instNatCast Top.top instTopENat	—	coheight_coe_withTop coheight_nat top_add
coheight_coe_withBot 📖	mathematical	—	coheight WithBot WithBot.instPreorder WithBot.some	—	height_coe_withTop
coheight_coe_withTop 📖	mathematical	—	coheight WithTop WithTop.instPreorder WithTop.some ENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_coe_withBot
coheight_eq 📖	mathematical	—	coheight iSup ENat LTSeries ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Preorder.toLE RelSeries.head setOf Preorder.toLT ENat.instNatCast RelSeries.length	—	Equiv.iSup_congr RelSeries.reverse_reverse iSup_congr_Prop
coheight_eq_coe_add_one_iff 📖	mathematical	—	coheight ENat instAddENat ENat.instNatCast AddMonoidWithOne.toOne instAddMonoidWithOneENat instLTENat Top.top instTopENat Preorder.toLT instLEENat	—	height_eq_coe_add_one_iff
coheight_eq_coe_iff 📖	mathematical	—	coheight ENat ENat.instNatCast instLTENat Top.top instTopENat Preorder.toLT instSubENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_eq_coe_iff
coheight_eq_coe_iff_maximal_le_coheight 📖	mathematical	—	coheight ENat ENat.instNatCast Maximal Preorder.toLE instLEENat	—	height_eq_coe_iff_minimal_le_height
coheight_eq_iSup_gt_coheight 📖	mathematical	—	coheight iSup ENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Preorder.toLT instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_eq_iSup_lt_height
coheight_eq_iSup_head_eq 📖	mathematical	—	coheight iSup ENat LTSeries ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat RelSeries.head setOf Preorder.toLT ENat.instNatCast RelSeries.length	—	height_eq_iSup_last_eq Equiv.iSup_congr RelSeries.reverse_reverse iSup_congr_Prop RelSeries.head_reverse
coheight_eq_index_of_length_eq_head_coheight 📖	mathematical	ENat ENat.instNatCast RelSeries.length setOf Preorder.toLT coheight RelSeries.head	coheight RelSeries.toFun setOf Preorder.toLT ENat ENat.instNatCast RelSeries.length	—	height_eq_index_of_length_eq_height_last RelSeries.last_reverse
coheight_eq_krullDim_Ici 📖	mathematical	—	WithBot.some ENat coheight krullDim Set.Elem Set.Ici Subtype.preorder Set Set.instMembership	—	coheight.eq_1 krullDim_orderDual krullDim_eq_of_orderIso height_eq_krullDim_Iic
coheight_eq_top_iff 📖	mathematical	—	coheight Top.top ENat instTopENat LTSeries RelSeries.head setOf Preorder.toLT RelSeries.length	—	RelSeries.last_reverse RelSeries.head_reverse height_eq_top_iff
coheight_eq_zero 📖	mathematical	—	coheight ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMax Preorder.toLE	—	height_eq_zero
coheight_int 📖	mathematical	—	coheight PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Top.top ENat instTopENat	—	coheight_of_noMaxOrder LinearOrderedAddCommGroup.to_noMaxOrder Int.instIsOrderedAddMonoid Infinite.instNontrivial Int.infinite
coheight_le 📖	mathematical	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT	ENat instLEENat coheight	—	coheight_le_iff'
coheight_le_coe_iff 📖	mathematical	—	ENat instLEENat coheight ENat.instNatCast instLTENat	—	height_le_coe_iff
coheight_le_coheight_apply_of_strictMono 📖	mathematical	StrictMono	ENat instLEENat coheight	—	height_le_height_apply_of_strictMono
coheight_le_iff 📖	mathematical	—	ENat instLEENat coheight ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	coheight_eq iSup₂_le_iff
coheight_le_iff' 📖	mathematical	—	ENat instLEENat coheight ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	coheight_eq_iSup_head_eq iSup₂_le_iff
coheight_le_krullDim 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.some coheight krullDim	—	krullDim_orderDual height_le_krullDim
coheight_le_of_krullDim_preimage_le 📖	mathematical	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom PartialOrder.toPreorder OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership WithBot.natCast ENat.instNatCast	ENat instLEENat coheight instAddENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast AddMonoidWithOne.toOne instAddMonoidWithOneENat PartialOrder.toPreorder DFunLike.coe OrderHom OrderHom.instFunLike	—	coheight.eq_1 height_le_of_krullDim_preimage_le krullDim_orderDual
coheight_nat 📖	mathematical	—	coheight Nat.instPreorder Top.top ENat instTopENat	—	coheight_of_noMaxOrder Nat.instNoMaxOrder
coheight_ne_zero 📖	mathematical	—	IsMax Preorder.toLE	—	Iff.not coheight_eq_zero
coheight_ofDual 📖	mathematical	—	coheight DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual height OrderDual.instPreorder	—	—
coheight_of_noMaxOrder 📖	mathematical	—	coheight Top.top ENat instTopENat	—	Nat.exists_strictMono Set.nonempty_Ioi_subtype Set.instNoMaxOrderElemIoi coheight_eq_top_iff Subtype.prop
coheight_orderIso 📖	mathematical	—	coheight DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso	—	height_orderIso
coheight_pos 📖	mathematical	—	ENat instLTENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat coheight IsMax Preorder.toLE	—	—
coheight_pos_of_lt_top 📖	mathematical	Preorder.toLT Top.top OrderTop.toTop Preorder.toLE	ENat instLTENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat coheight	—	coheight_pos
coheight_strictAnti 📖	mathematical	Preorder.toLT ENat instLTENat coheight Top.top instTopENat	ENat instLTENat coheight	—	height_strictMono
coheight_toDual 📖	mathematical	—	coheight OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual height	—	—
coheight_top 📖	mathematical	—	coheight Top.top OrderTop.toTop Preorder.toLE ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
exists_series_of_coheight_eq_coe 📖	mathematical	coheight ENat ENat.instNatCast	LTSeries RelSeries.head setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_coheight le_of_eq
exists_series_of_height_eq_coe 📖	mathematical	height ENat ENat.instNatCast	LTSeries RelSeries.last setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_height le_of_eq
exists_series_of_le_coheight 📖	mathematical	ENat instLEENat ENat.instNatCast coheight	LTSeries RelSeries.head setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_height
exists_series_of_le_height 📖	mathematical	ENat instLEENat ENat.instNatCast height	LTSeries RelSeries.last setOf Preorder.toLT RelSeries.length	—	Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_and_eq RelSeries.last_drop bddAbove_def ENat.iSup_coe_eq_top iSup_subtype' height_eq_iSup_last_eq Nat.cast_le IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
finiteDimensionalOrder_iff_krullDim_ne_bot_and_top 📖	mathematical	—	FiniteDimensionalOrder	—	LTSeries.nonempty_of_finiteDimensionalOrder krullDim_eq_bot_iff not_nonempty_iff
height_add_one_le 📖	mathematical	Preorder.toLT	ENat instLEENat instAddENat height AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_mono le_of_lt top_add add_one_le_of_lt height_strictMono
height_bot 📖	mathematical	—	height Bot.bot OrderBot.toBot Preorder.toLE ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
height_coe_withBot 📖	mathematical	—	height WithBot WithBot.instPreorder WithBot.some ENat instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	le_antisymm height_le ne_bot_of_gt LTSeries.strictMono compare_gt_iff_gt WithBot.coe_unbot RelSeries.step length_le_height_last Nat.cast_one Nat.cast_zero iSup₂_le WithBot.coe_strictMono le_iSup₂_of_le RelSeries.last_cons instReflLe RelSeries.cons_length Nat.cast_add
height_coe_withTop 📖	mathematical	—	height WithTop WithTop.instPreorder WithTop.some	—	le_antisymm height_le WithTop.lt_top_iff_ne_top lt_of_le_of_lt LTSeries.monotone RelSeries.last.eq_1 WithTop.coe_untop RelSeries.step length_le_height_last WithTop.coe_strictMono le_iSup₂_of_le instReflLe
height_enat 📖	mathematical	—	height ENat instPreorderENat	—	height_top_eq_krullDim krullDim_enat height_coe_withTop height_nat
height_eq_coe_add_one_iff 📖	mathematical	—	height ENat instAddENat ENat.instNatCast AddMonoidWithOne.toOne instAddMonoidWithOneENat instLTENat Top.top instTopENat Preorder.toLT instLEENat	—	le_antisymm_iff coe_lt_height_iff Nat.cast_add Nat.cast_one height_le_coe_iff
height_eq_coe_iff 📖	mathematical	—	height ENat ENat.instNatCast instLTENat Top.top instTopENat Preorder.toLT instSubENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Nat.cast_zero zero_tsub Nat.cast_add Nat.cast_one Unique.instSubsingleton height_eq_coe_add_one_iff IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
height_eq_coe_iff_minimal_le_height 📖	mathematical	—	height ENat ENat.instNatCast Minimal Preorder.toLE instLEENat	—	Nat.cast_zero Nat.cast_add Nat.cast_one RelSeries.eraseLast_last_rel_last add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid length_le_height_last
height_eq_iSup_last_eq 📖	mathematical	—	height iSup ENat LTSeries ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat RelSeries.last setOf Preorder.toLT ENat.instNatCast RelSeries.length	—	eq_of_forall_ge_iff height_le_iff' iSup₂_le_iff
height_eq_iSup_lt_height 📖	mathematical	—	height iSup ENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Preorder.toLT instAddENat AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	le_antisymm height_le Nat.cast_zero le_iSup_of_le RelSeries.eraseLast_last_rel_last le_iSup₂_of_le Nat.cast_add Nat.cast_one add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid instReflLe iSup₂_le RelSeries.last_snoc
height_eq_index_of_length_eq_height_last 📖	mathematical	ENat ENat.instNatCast RelSeries.length setOf Preorder.toLT height RelSeries.last	height RelSeries.toFun setOf Preorder.toLT ENat ENat.instNatCast RelSeries.length	—	le_antisymm height_le RelSeries.head_drop length_le_height_last IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid Nat.cast_add RelSeries.last_smash RelSeries.last_drop index_le_height
height_eq_krullDim_Iic 📖	mathematical	—	WithBot.some ENat height krullDim Set.Elem Set.Iic Subtype.preorder Set Set.instMembership	—	height_top_eq_krullDim height.eq_1 le_antisymm iSup_le le_trans LTSeries.monotone LTSeries.strictMono iSup_congr_Prop iSup_pos le_iSup LTSeries.map_length le_iSup₂
height_eq_top_iff 📖	mathematical	—	height Top.top ENat instTopENat LTSeries RelSeries.last setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_height height_eq_iSup_last_eq iSup_subtype' ENat.iSup_coe_eq_top bddAbove_def Mathlib.Tactic.Push.not_forall_eq IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd
height_eq_zero 📖	mathematical	—	height ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMin Preorder.toLE	—	Nat.cast_zero height_le_coe_iff
height_int 📖	mathematical	—	height PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Top.top ENat instTopENat	—	height_of_noMinOrder LinearOrderedAddCommGroup.to_noMinOrder Int.instIsOrderedAddMonoid Infinite.instNontrivial Int.infinite
height_le 📖	mathematical	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT	ENat instLEENat height	—	height_le_iff lt_of_lt_of_le RelSeries.eraseLast_last_rel_last RelSeries.last_snoc Nat.cast_zero
height_le_coe_iff 📖	mathematical	—	ENat instLEENat height ENat.instNatCast instLTENat	—	height_eq_iSup_lt_height iSup₂_le_iff top_add Nat.cast_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
height_le_height_apply_of_strictMono 📖	mathematical	StrictMono	ENat instLEENat height	—	height_eq_iSup_last_eq iSup_congr_Prop iSup₂_le le_iSup₂_of_le instReflLe
height_le_iff 📖	mathematical	—	ENat instLEENat height ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	height.eq_1 iSup₂_le_iff
height_le_iff' 📖	mathematical	—	ENat instLEENat height ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	height_le_iff le_of_eq height_le
height_le_krullDim 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.some height krullDim	—	krullDim_eq_iSup_length height_le le_iSup_of_le le_rfl
height_le_of_krullDim_preimage_le 📖	mathematical	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom PartialOrder.toPreorder OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership WithBot.natCast ENat.instNatCast	ENat instLEENat height instAddENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast AddMonoidWithOne.toOne instAddMonoidWithOneENat PartialOrder.toPreorder DFunLike.coe OrderHom OrderHom.instFunLike	—	ENat.mul_top Unique.instSubsingleton NeZero.one top_add Nat.strong_induction_on height_le_iff le_of_not_gt LE.le.lt_of_not_ge OrderHom.monotone LE.le.trans LTSeries.monotone le_antisymm le_trans RelSeries.last_drop RelSeries.head_drop RelSeries.step LTSeries.length_le_krullDim ENat.coe_lt_coe LE.le.trans_lt le_add_left le_rfl WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass WithBot.charZero Nat.instOrderedSub ENat.ne_top_iff_exists LT.lt.ne height_mono LT.lt.le ENat.coe_lt_top height_strictMono length_le_height_last not_lt_of_ge add_le_add_left covariant_swap_add_of_covariant_add mul_le_mul_right CanonicallyOrderedAdd.toMulLeftMono ENat.coe_one ENat.coe_add ENat.coe_le_coe LT.lt.trans_le mul_add_one Distrib.leftDistribClass add_assoc add_comm tsub_le_iff_right Nat.cast_one Nat.cast_add ENat.coe_sub RelSeries.take_length
height_mono 📖	mathematical	—	Monotone ENat instPreorderENat height	—	biSup_mono LE.le.trans
height_nat 📖	mathematical	—	height Nat.instPreorder ENat ENat.instNatCast	—	le_antisymm height_le_coe_iff IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid length_le_height_last
height_ne_zero 📖	mathematical	—	IsMin Preorder.toLE	—	Iff.not height_eq_zero
height_ofDual 📖	mathematical	—	height DFunLike.coe Equiv OrderDual EquivLike.toFunLike Equiv.instEquivLike OrderDual.ofDual coheight OrderDual.instPreorder	—	—
height_of_noMinOrder 📖	mathematical	—	height Top.top ENat instTopENat	—	coheight_of_noMaxOrder OrderDual.noMaxOrder
height_orderIso 📖	mathematical	—	height DFunLike.coe OrderIso Preorder.toLE instFunLikeOrderIso	—	le_antisymm OrderIso.symm_apply_apply height_le_height_apply_of_strictMono OrderIso.strictMono
height_pos 📖	mathematical	—	ENat instLTENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat height IsMin Preorder.toLE	—	—
height_pos_of_bot_lt 📖	mathematical	Preorder.toLT Bot.bot OrderBot.toBot Preorder.toLE	ENat instLTENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat height	—	height_pos
height_strictMono 📖	mathematical	Preorder.toLT ENat instLTENat height Top.top instTopENat	ENat instLTENat height	—	ENat.add_one_le_iff LT.lt.ne iSup₂_le_iff length_le_height_last Nat.cast_add Nat.cast_one RelSeries.last_snoc
height_toDual 📖	mathematical	—	height OrderDual OrderDual.instPreorder DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike OrderDual.toDual coheight	—	—
height_top_eq_krullDim 📖	mathematical	—	WithBot.some ENat height Top.top OrderTop.toTop Preorder.toLE krullDim	—	krullDim_eq_iSup_length top_nonempty le_antisymm height_le le_iSup_of_le le_rfl iSup_le length_le_height le_top
index_le_height 📖	mathematical	—	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT height RelSeries.toFun	—	length_le_height_last
instKrullDimLEOfNatNatOfSubsingleton 📖	mathematical	—	KrullDimLE	—	krullDim_nonpos_of_subsingleton
krullDimLE_iff 📖	mathematical	—	KrullDimLE WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.natCast ENat.instNatCast	—	—
krullDim_WithTop 📖	mathematical	—	krullDim WithTop WithTop.instPreorder WithBot ENat WithBot.add instAddENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	height_top_eq_krullDim krullDim_eq_iSup_height_of_nonempty height_eq_iSup_lt_height iSup_congr_Prop Nat.cast_one ENat.iSup_add iSup_subtype' Equiv.iSup_congr height_coe_withTop
krullDim_enat 📖	mathematical	—	krullDim ENat instPreorderENat Top.top WithBot WithBot.instTop instTopENat	—	krullDim_WithTop krullDim_of_noMaxOrder Nat.instNoMaxOrder top_add
krullDim_eq_bot 📖	mathematical	—	krullDim Bot.bot WithBot ENat WithBot.bot	—	krullDim_eq_bot_iff
krullDim_eq_bot_iff 📖	mathematical	—	krullDim Bot.bot WithBot ENat WithBot.bot IsEmpty	—	eq_bot_iff krullDim.eq_1 iSup_le_iff Fin.isEmpty'
krullDim_eq_iSup_coheight 📖	mathematical	—	krullDim iSup WithBot ENat WithBot.instSupSet instPreorderENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.some coheight	—	isEmpty_or_nonempty krullDim_eq_bot ciSup_of_empty krullDim_eq_iSup_coheight_of_nonempty WithBot.coe_iSup OrderTop.bddAbove
krullDim_eq_iSup_coheight_of_nonempty 📖	mathematical	—	krullDim WithBot.some ENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight	—	krullDim_orderDual krullDim_eq_iSup_height_of_nonempty OrderDual.instNonempty
krullDim_eq_iSup_height 📖	mathematical	—	krullDim iSup WithBot ENat WithBot.instSupSet instPreorderENat ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.some height	—	isEmpty_or_nonempty krullDim_eq_bot ciSup_of_empty krullDim_eq_iSup_height_of_nonempty WithBot.coe_iSup OrderTop.bddAbove
krullDim_eq_iSup_height_add_coheight_of_nonempty 📖	mathematical	—	krullDim WithBot.some ENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instAddENat height coheight	—	le_antisymm krullDim_eq_iSup_height_of_nonempty WithBot.coe_le_coe ciSup_mono OrderTop.bddAbove krullDim_eq_iSup_length iSup_le WithBot.coe_lt_coe lt_of_le_of_lt height_le_krullDim coheight_le_krullDim exists_series_of_height_eq_coe exists_series_of_coheight_eq_coe le_iSup_of_le Nat.cast_add instReflLe
krullDim_eq_iSup_height_of_nonempty 📖	mathematical	—	krullDim WithBot.some ENat iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height	—	le_antisymm iSup_le le_iSup_of_le length_le_height_last WithBot.unbotD_le_iff WithBot.coe_iSup OrderTop.bddAbove height_le_krullDim
krullDim_eq_iSup_length 📖	mathematical	—	krullDim WithBot.some ENat iSup LTSeries ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	WithBot.coe_iSup OrderTop.bddAbove RelSeries.instNonempty
krullDim_eq_length_of_finiteDimensionalOrder 📖	mathematical	—	krullDim WithBot ENat WithBot.natCast ENat.instNatCast RelSeries.length setOf Preorder.toLT LTSeries.longestOf	—	le_antisymm iSup_le WithBot.coe_le_coe WithTop.coe_le_coe RelSeries.length_le_length_longestOf le_iSup
krullDim_eq_of_orderIso 📖	mathematical	—	krullDim	—	le_antisymm krullDim_le_of_strictMono OrderIso.strictMono
krullDim_eq_one_iff_of_boundedOrder 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat IsSimpleOrder Preorder.toLE	—	le_antisymm_iff krullDim_le_one_iff_of_boundedOrder WithBot.one_le_iff_pos NeZero.one krullDim_pos_iff_of_orderBot isSimpleOrder_iff
krullDim_eq_top 📖	mathematical	—	krullDim Top.top WithBot ENat WithBot.instTop instTopENat	—	le_antisymm le_top le_iSup_iff not_le_of_gt WithBot.bot_lt_coe le_refl not_lt_of_ge WithBot.some_eq_coe WithBot.coe_natCast WithBot.coe_lt_coe WithTop.some_eq_coe WithTop.coe_natCast WithTop.coe_lt_coe LTSeries.length_withLength Nat.cast_add Nat.cast_one IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd
krullDim_eq_top_iff 📖	mathematical	—	krullDim Top.top WithBot ENat WithBot.instTop instTopENat InfiniteDimensionalOrder	—	isEmpty_or_nonempty krullDim_eq_bot WithBot.nontrivial finiteDimensionalOrder_or_infiniteDimensionalOrder krullDim_eq_length_of_finiteDimensionalOrder krullDim_eq_top
krullDim_eq_zero 📖	mathematical	—	krullDim WithBot ENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg
krullDim_eq_zero_iff_of_orderBot 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_bot_iff krullDim_nonpos_iff_forall_isMax Eq.le bot_le krullDim_eq_zero bot_nonempty
krullDim_eq_zero_iff_of_orderTop 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	top_le_iff krullDim_nonpos_iff_forall_isMin Eq.le le_top krullDim_eq_zero top_nonempty
krullDim_eq_zero_of_unique 📖	mathematical	—	krullDim WithBot ENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	le_antisymm krullDim_nonpos_of_subsingleton Unique.instSubsingleton krullDim_nonneg
krullDim_int 📖	mathematical	—	krullDim PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt Top.top WithBot ENat WithBot.instTop instTopENat	—	krullDim_of_noMaxOrder LinearOrderedAddCommGroup.to_noMaxOrder Int.instIsOrderedAddMonoid Infinite.instNontrivial Int.infinite
krullDim_le_of_krullDim_preimage_le 📖	mathematical	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom PartialOrder.toPreorder OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership WithBot.natCast ENat.instNatCast	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.add instAddENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring WithBot.instCommSemiring LinearOrder.toDecidableEq instLinearOrderENat instCommSemiringENat ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instCanonicallyOrderedAddENat instNoZeroDivisorsENat instNontrivialENat WithBot.natCast ENat.instNatCast WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat PartialOrder.toPreorder	—	krullDim_eq_iSup_height iSup_le_iff LE.le.trans WithBot.coe_mono height_le_of_krullDim_preimage_le add_le_add_left WithBot.addRightMono covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_le_mul_of_nonneg_left WithBot.instPosMulMono IsOrderedRing.toPosMulMono le_iSup_iff right_eq_inf
krullDim_le_of_krullDim_preimage_le' 📖	mathematical	Monotone PartialOrder.toPreorder WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim Set.Elem Set.preimage Set Set.instSingletonSet Subtype.preorder Set.instMembership WithBot.natCast ENat.instNatCast	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.add instAddENat Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring WithBot.instCommSemiring LinearOrder.toDecidableEq instLinearOrderENat instCommSemiringENat ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instCanonicallyOrderedAddENat instNoZeroDivisorsENat instNontrivialENat WithBot.natCast ENat.instNatCast WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat PartialOrder.toPreorder	—	krullDim_le_of_krullDim_preimage_le
krullDim_le_of_strictComono_and_surj 📖	mathematical	Preorder.toLT	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim	—	iSup_le le_sSup
krullDim_le_of_strictMono 📖	mathematical	StrictMono	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim	—	iSup_le le_sSup
krullDim_le_one_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat IsMin IsMax	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.not_ge Nat.cast_zero WithBot.zeroLEOneClass zero_add Nat.cast_one instReflLe Fintype.complete Nat.instAtLeastTwoHAddOfNat WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.charZero
krullDim_le_one_iff_forall_isMax 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim PartialOrder.toPreorder WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat IsMax	—	—
krullDim_le_one_iff_forall_isMin 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim PartialOrder.toPreorder WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat IsMin	—	—
krullDim_le_one_iff_of_boundedOrder 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim PartialOrder.toPreorder WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat Bot.bot OrderBot.toBot BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	—
krullDim_lt_coe_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat krullDim WithBot.natCast ENat.instNatCast RelSeries.length setOf	—	krullDim.eq_1 WithBot.coe_natCast ENat.coe_zero bot_eq_zero WithBot.lt_coe_bot Nat.instCanonicallyOrderedAdd Nat.cast_add Nat.cast_one WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass WithBot.charZero Nat.instNoMaxOrder
krullDim_nat 📖	mathematical	—	krullDim Nat.instPreorder Top.top WithBot ENat WithBot.instTop instTopENat	—	krullDim_of_noMaxOrder Nat.instNoMaxOrder
krullDim_ne_bot_iff 📖	—	—	—	—	krullDim_eq_bot_iff not_isEmpty_iff
krullDim_ne_bot_of_finiteDimensionalOrder 📖	—	—	—	—	finiteDimensionalOrder_iff_krullDim_ne_bot_and_top
krullDim_ne_top_of_finiteDimensionalOrder 📖	—	—	—	—	finiteDimensionalOrder_iff_krullDim_ne_bot_and_top
krullDim_nonneg 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim	—	krullDim_nonneg_iff
krullDim_nonneg_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ krullDim_eq_bot_iff WithBot.lt_coe_bot bot_eq_zero WithBot.coe_zero
krullDim_nonpos_iff_forall_isMax 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMax	—	LE.le.not_gt Matrix.cons_val_fin_one Nat.cast_one WithBot.zeroLEOneClass NeZero.one WithBot.nontrivial Nat.cast_zero instReflLe
krullDim_nonpos_iff_forall_isMin 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMin	—	—
krullDim_nonpos_of_subsingleton 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat krullDim WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	krullDim_nonpos_iff_forall_isMax Eq.ge
krullDim_of_isSimpleOrder 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	krullDim_eq_one_iff_of_boundedOrder
krullDim_of_noMaxOrder 📖	mathematical	—	krullDim Top.top WithBot ENat WithBot.instTop instTopENat	—	krullDim_eq_iSup_coheight coheight_of_noMaxOrder ciSup_const
krullDim_of_noMinOrder 📖	mathematical	—	krullDim Top.top WithBot ENat WithBot.instTop instTopENat	—	krullDim_eq_iSup_height height_of_noMinOrder ciSup_const
krullDim_orderDual 📖	mathematical	—	krullDim OrderDual OrderDual.instPreorder	—	le_antisymm iSup_le le_sSup
krullDim_pos_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim	—	Mathlib.Tactic.Contrapose.contrapose_iff₁
krullDim_pos_iff_of_orderBot 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim PartialOrder.toPreorder Nontrivial	—	not_subsingleton_iff_nontrivial krullDim_eq_zero_iff_of_orderBot lt_or_lt_iff_ne bot_nonempty
krullDim_pos_iff_of_orderTop 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder instPreorderENat WithBot.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim PartialOrder.toPreorder Nontrivial	—	not_subsingleton_iff_nontrivial krullDim_eq_zero_iff_of_orderTop lt_or_lt_iff_ne top_nonempty
krullDim_withBot 📖	mathematical	—	krullDim WithBot WithBot.instPreorder ENat WithBot.add instAddENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	krullDim_orderDual krullDim_WithTop OrderDual.instNonempty
le_krullDim_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.natCast ENat.instNatCast krullDim LTSeries RelSeries.length setOf Preorder.toLT	—	isEmpty_or_nonempty krullDim_eq_bot RelSeries.instIsEmpty finiteDimensionalOrder_or_infiniteDimensionalOrder krullDim_eq_length_of_finiteDimensionalOrder Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass WithBot.charZero LTSeries.longestOf_is_longest krullDim_eq_top SetRel.InfiniteDimensional.exists_relSeries_with_length
length_le_coheight 📖	mathematical	Preorder.toLE RelSeries.head setOf Preorder.toLT	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT coheight	—	length_le_height RelSeries.last_reverse
length_le_coheight_head 📖	mathematical	—	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT coheight RelSeries.head	—	length_le_coheight le_rfl
length_le_height 📖	mathematical	Preorder.toLE RelSeries.last setOf Preorder.toLT	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT height	—	lt_of_lt_of_le RelSeries.step le_iSup₂_of_le RelSeries.last_snoc instReflLe le_rfl Nat.cast_one Nat.cast_add Nat.cast_zero
length_le_height_last 📖	mathematical	—	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT height RelSeries.last	—	length_le_height le_rfl
one_le_krullDim_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.one AddMonoidWithOne.toOne instAddMonoidWithOneENat krullDim Preorder.toLT	—	krullDim_pos_iff Nat.cast_zero ENat.WithBot.add_one_le_iff zero_add
one_lt_height_iff 📖	mathematical	—	ENat instLTENat AddMonoidWithOne.toOne instAddMonoidWithOneENat height Preorder.toLT	—	ENat.add_one_le_iff ENat.one_ne_top Nat.instAtLeastTwoHAddOfNat one_add_one_eq_two exists_series_of_le_height RelSeries.rel_of_lt SetRel.instIsTransSetOfProdMatch_1PropOfIsTrans instIsTransLt Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd instReflLe List.isChain_pair RelSeries.toList_fromListIsChain length_le_height Eq.le
rev_index_le_coheight 📖	mathematical	—	ENat instLEENat ENat.instNatCast RelSeries.length setOf Preorder.toLT coheight RelSeries.toFun	—	index_le_height

Order.IsMax

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coheight_eq_zero 📖	mathematical	IsMax Preorder.toLE	Order.coheight ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Order.coheight_eq_zero

Order.IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_eq_zero 📖	mathematical	IsMin Preorder.toLE	Order.height ENat MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Order.height_eq_zero

Order.KrullDimLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
krullDim_le 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat Order.krullDim WithBot.natCast ENat.instNatCast	—	—
mono 📖	mathematical	—	Order.KrullDimLE	—	LE.le.trans krullDim_le Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass WithBot.charZero

Order.LTSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_le_krullDim 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder instPreorderENat WithBot.natCast ENat.instNatCast RelSeries.length setOf Preorder.toLT Order.krullDim	—	le_sSup

---

← Back to Index