Commit 2024-11-18 11:19 bcef7c52

View on Github →

feat(KrullDimension): coheight API (#19148) Part of #15524. This adds basic definitions for the coheight, and then analogous lemmas for every lemma about height. Due to the way coheight is defined, most lemmas are defeq to the corresponding lemma bout height in the dual order. From the Carleson project.

Estimated changes

Modified Mathlib/Order/KrullDimension.lean

added theorem Order.coe_lt_coheight_iff

added theorem Order.coheight_anti

added theorem Order.coheight_eq

added theorem Order.coheight_eq_coe_add_one_iff

added theorem Order.coheight_eq_coe_iff

added theorem Order.coheight_eq_coe_iff_maximal_le_coheight

added theorem Order.coheight_eq_iSup_gt_coheight

added theorem Order.coheight_eq_iSup_head_eq

added theorem Order.coheight_eq_index_of_length_eq_head_coheight

added theorem Order.coheight_eq_top_iff

added theorem Order.coheight_eq_zero

added theorem Order.coheight_le

added theorem Order.coheight_le_coe_iff

added theorem Order.coheight_le_coheight_apply_of_strictMono

added theorem Order.coheight_le_iff'

added theorem Order.coheight_le_iff

added theorem Order.coheight_ofDual

added theorem Order.coheight_orderIso

added theorem Order.coheight_toDual

added theorem Order.coheight_top

added theorem Order.exists_series_of_coheight_eq_coe

added theorem Order.exists_series_of_le_coheight

modified theorem Order.height_le_coe_iff

added theorem Order.height_ofDual

added theorem Order.height_toDual

added theorem Order.length_le_coheight

added theorem Order.length_le_coheight_head

added theorem Order.rev_index_le_coheight