Commit 2026-03-06 05:52 fad8d3ad

View on Github →

feat(Data): some lemmas about WithBot ENat (#28582) Add some lemma about withBot ENat discovered when dealing with ringKrullDim

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem AddLECancellable.withBot

added theorem AddLECancellable.withTop

added theorem IsAddLeftRegular.withBot

added theorem IsAddLeftRegular.withTop

added theorem IsAddRightRegular.withBot

added theorem IsAddRightRegular.withTop

Modified Mathlib/CategoryTheory/Abelian/Injective/Dimension.lean

Modified Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.WithBot.add_le_add_natCast_left_iff

added theorem ENat.WithBot.add_le_add_natCast_right_iff

added theorem ENat.WithBot.add_le_add_one_left_iff

added theorem ENat.WithBot.add_le_add_one_right_iff

added theorem ENat.WithBot.add_natCast_cancel

added theorem ENat.WithBot.add_ofNat_cancel

added theorem ENat.WithBot.add_one_cancel

added theorem ENat.WithBot.add_one_le_iff

added theorem ENat.WithBot.lt_add_one_iff

added theorem ENat.WithBot.natCast_add_cancel

added theorem ENat.WithBot.ofNat_add_cancel

added theorem ENat.WithBot.one_add_cancel

deleted theorem WithBot.add_one_le_iff

deleted theorem WithBot.lt_add_one_iff

Modified Mathlib/Order/KrullDimension.lean