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	42 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_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
height 📖	CompOp	46 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_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, 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
krullDim 📖	CompOp	57 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, 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_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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Bot.bot WithBot.bot krullDim	—	bot_lt_krullDim_iff
bot_lt_krullDim_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Bot.bot WithBot.bot krullDim	—	bot_lt_iff_ne_bot krullDim_ne_bot_iff
coe_lt_coheight_iff 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight Top.top instTopENat	ENat.instNatCast	—	coe_lt_height_iff
coe_lt_height_iff 📖	mathematical	ENat Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height Top.top instTopENat	ENat.instNatCast	—	LT.lt.ne_top exists_series_of_height_eq_coe IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass 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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat coheight AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	coheight_anti le_of_lt top_add add_one_le_of_lt coheight_strictAnti
coheight_anti 📖	mathematical	—	Antitone ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Top.top instTopENat Preorder.toLE	—	height_eq_coe_add_one_iff
coheight_eq_coe_iff 📖	mathematical	—	coheight ENat ENat.instNatCast Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Top.top instTopENat instSubENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	height_eq_coe_iff
coheight_eq_coe_iff_maximal_le_coheight 📖	mathematical	—	coheight ENat ENat.instNatCast Maximal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	—	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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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	RelSeries.toFun	—	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 RelSeries.head setOf Preorder.toLT RelSeries.length	—	RelSeries.last_reverse RelSeries.head_reverse height_eq_top_iff
coheight_eq_zero 📖	mathematical	—	coheight ENat instZeroENat 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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast RelSeries.length setOf Preorder.toLT	coheight	—	coheight_le_iff'
coheight_le_coe_iff 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight ENat.instNatCast Preorder.toLT	—	height_le_coe_iff
coheight_le_coheight_apply_of_strictMono 📖	mathematical	StrictMono	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight	—	height_le_height_apply_of_strictMono
coheight_le_iff 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	coheight_eq iSup₂_le_iff
coheight_le_iff' 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.some coheight krullDim	—	krullDim_orderDual height_le_krullDim
coheight_le_of_krullDim_preimage_le 📖	mathematical	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	coheight Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul ENat.instNatCast AddMonoidWithOne.toOne	—	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 Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instZeroENat coheight IsMax Preorder.toLE	—	—
coheight_pos_of_lt_top 📖	mathematical	Preorder.toLT Top.top OrderTop.toTop Preorder.toLE	ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instZeroENat coheight	—	coheight_pos
coheight_strictAnti 📖	—	Preorder.toLT ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat coheight Top.top instTopENat	—	—	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 instZeroENat	—	—
exists_series_of_coheight_eq_coe 📖	mathematical	coheight ENat ENat.instNatCast	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	RelSeries.last setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_height le_of_eq
exists_series_of_le_coheight 📖	mathematical	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast coheight	RelSeries.head setOf Preorder.toLT RelSeries.length	—	exists_series_of_le_height RelSeries.head_reverse
exists_series_of_le_height 📖	mathematical	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast height	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 IsOrderedRing.toZeroLEOneClass
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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat height AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 instZeroENat	—	—
height_coe_withBot 📖	mathematical	—	height WithBot WithBot.instPreorder WithBot.some ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 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
height_enat 📖	mathematical	—	height ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	—	height_top_eq_krullDim krullDim_enat height_coe_withTop height_nat
height_eq_coe_add_one_iff 📖	mathematical	—	height ENat Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat ENat.instNatCast AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Top.top instTopENat Preorder.toLE	—	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 Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Top.top instTopENat instSubENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Nat.cast_zero zero_tsub Nat.cast_add Nat.cast_one Unique.instSubsingleton height_eq_coe_add_one_iff IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
height_eq_coe_iff_minimal_le_height 📖	mathematical	—	height ENat ENat.instNatCast Minimal Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat	—	Nat.cast_zero Nat.cast_add Nat.cast_one RelSeries.eraseLast_last_rel_last add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd 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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid 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	RelSeries.toFun	—	le_antisymm height_le RelSeries.head_drop length_le_height_last IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass 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 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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass
height_eq_zero 📖	mathematical	—	height ENat instZeroENat 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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast RelSeries.length setOf Preorder.toLT	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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height ENat.instNatCast Preorder.toLT	—	height_eq_iSup_lt_height iSup₂_le_iff top_add Nat.cast_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass
height_le_height_apply_of_strictMono 📖	mathematical	StrictMono	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height	—	height_eq_iSup_last_eq iSup_congr_Prop iSup₂_le le_iSup₂_of_le
height_le_iff 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height ENat.instNatCast RelSeries.length setOf Preorder.toLT	—	height.eq_1 iSup₂_le_iff
height_le_iff' 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	height Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul ENat.instNatCast AddMonoidWithOne.toOne	—	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 IsOrderedRing.toZeroLEOneClass 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 IsOrderedRing.toZeroLEOneClass 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 Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instZeroENat height IsMin Preorder.toLE	—	—
height_pos_of_bot_lt 📖	mathematical	Preorder.toLT Bot.bot OrderBot.toBot Preorder.toLE	ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat instZeroENat height	—	height_pos
height_strictMono 📖	—	Preorder.toLT ENat PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat height Top.top instTopENat	—	—	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 Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
krullDim_WithTop 📖	mathematical	—	krullDim WithTop WithTop.instPreorder WithBot ENat WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ConditionallyCompletePartialOrderSup.toSupSet 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ConditionallyCompletePartialOrderSup.toSupSet 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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat 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
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 AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat 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 AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsSimpleOrder Preorder.toLE	—	le_antisymm_iff krullDim_le_one_iff_of_boundedOrder WithBot.one_le_iff_pos IsOrderedRing.toZeroLEOneClass 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 AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass
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 instZeroENat	—	le_antisymm krullDim_nonpos_of_subsingleton krullDim_nonneg
krullDim_eq_zero_iff_of_orderBot 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.zero instZeroENat	—	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 instZeroENat	—	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 instZeroENat	—	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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim Set.Elem Set.preimage DFunLike.coe OrderHom OrderHom.instFunLike Set Set.instSingletonSet Subtype.preorder Set.instMembership AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul WithBot.instCommSemiring LinearOrder.toDecidableEq instLinearOrderENat instCanonicallyOrderedAddENat instNoZeroDivisorsENat instNontrivialENat WithBot.one AddMonoidWithOne.toOne	—	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 ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim Set.Elem Set.preimage Set Set.instSingletonSet Subtype.preorder Set.instMembership AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	WithBot.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul WithBot.instCommSemiring LinearOrder.toDecidableEq instLinearOrderENat instCanonicallyOrderedAddENat instNoZeroDivisorsENat instNontrivialENat WithBot.one AddMonoidWithOne.toOne	—	krullDim_le_of_krullDim_preimage_le
krullDim_le_of_strictComono_and_surj 📖	mathematical	Preorder.toLT	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim	—	iSup_le le_sSup
krullDim_le_of_strictMono 📖	mathematical	StrictMono	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim	—	iSup_le le_sSup
krullDim_le_one_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMin IsMax	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ Mathlib.Tactic.Push.not_forall_eq LT.lt.not_ge Nat.cast_zero WithBot.zeroLEOneClass IsOrderedRing.toZeroLEOneClass zero_add Nat.cast_one 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMax	—	—
krullDim_le_one_iff_forall_isMin 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat IsMin	—	—
krullDim_le_one_iff_of_boundedOrder 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Bot.bot OrderBot.toBot BoundedOrder.toOrderBot Top.top OrderTop.toTop BoundedOrder.toOrderTop	—	—
krullDim_lt_coe_iff 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat 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 IsOrderedRing.toZeroLEOneClass 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.zero instZeroENat krullDim	—	krullDim_nonneg_iff
krullDim_nonneg_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.zero instZeroENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.zero instZeroENat IsMax	—	LE.le.not_gt Matrix.cons_val_fin_one Nat.cast_one WithBot.zeroLEOneClass IsOrderedRing.toZeroLEOneClass NeZero.one WithBot.nontrivial Nat.cast_zero
krullDim_nonpos_iff_forall_isMin 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.zero instZeroENat IsMin	—	forall_swap
krullDim_nonpos_of_subsingleton 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat krullDim WithBot.zero instZeroENat	—	krullDim_nonpos_iff_forall_isMax Eq.ge
krullDim_of_isSimpleOrder 📖	mathematical	—	krullDim PartialOrder.toPreorder WithBot ENat WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.zero instZeroENat krullDim	—	Mathlib.Tactic.Contrapose.contrapose_iff₁
krullDim_pos_iff_of_orderBot 📖	mathematical	—	WithBot ENat Preorder.toLT WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.zero instZeroENat krullDim 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.zero instZeroENat krullDim 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 Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	krullDim_orderDual krullDim_WithTop OrderDual.instNonempty
le_krullDim_iff 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim 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 IsOrderedRing.toZeroLEOneClass 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast RelSeries.length coheight	—	length_le_height RelSeries.last_reverse
length_le_coheight_head 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat ENat.instNatCast RelSeries.length height	—	lt_of_lt_of_le RelSeries.step le_iSup₂_of_le RelSeries.last_snoc le_rfl Nat.cast_one Nat.cast_add Nat.cast_zero
length_le_height_last 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat WithBot.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat krullDim Preorder.toLT	—	krullDim_pos_iff Nat.cast_zero WithBot.add_one_le_iff zero_add
one_lt_height_iff 📖	mathematical	—	ENat Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat height	—	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.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instCharZero List.isChain_pair RelSeries.toList_fromListIsChain length_le_height Eq.le
rev_index_le_coheight 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat 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 instZeroENat	—	Order.coheight_eq_zero

Order.IsMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
height_eq_zero 📖	mathematical	IsMin Preorder.toLE	Order.height ENat instZeroENat	—	Order.height_eq_zero

Order.KrullDimLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
krullDim_le 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat Order.krullDim AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	—
mono 📖	mathematical	—	Order.KrullDimLE	—	LE.le.trans krullDim_le Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid WithBot.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithBot.charZero

Order.LTSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_le_krullDim 📖	mathematical	—	WithBot ENat Preorder.toLE WithBot.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrderENat AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat RelSeries.length setOf Preorder.toLT Order.krullDim	—	le_sSup

---

← Back to Index