Commit 2024-07-12 07:41 855a27b8

View on Github →

chore: move non @[to_additive] parts of Algebra.Order.Monoid and Algebra.Order.Group to a different file (#14667) Following the discussion on #14598, move LinearOrderedAddCommMonoidWithTop, LinearOrderedAddCommGroupWithTop, and associated theorems to Algebra.Order.AddGroupWithTop.

Estimated changes

added def WithBot.addHom
added theorem WithBot.add_bot
added theorem WithBot.add_eq_bot
added theorem WithBot.add_eq_coe
added theorem WithBot.add_ne_bot
added theorem WithBot.bot_add
added theorem WithBot.bot_lt_add
added theorem WithBot.bot_ne_natCast
added theorem WithBot.bot_ne_ofNat
added theorem WithBot.coe_add
added theorem WithBot.coe_addHom
added theorem WithBot.coe_eq_ofNat
added theorem WithBot.coe_natCast
added theorem WithBot.coe_nsmul
added theorem WithBot.coe_ofNat
added theorem WithBot.natCast_ne_bot
added theorem WithBot.ofNat_eq_coe
added theorem WithBot.ofNat_ne_bot
added def WithTop.addHom
added theorem WithTop.add_eq_coe
added theorem WithTop.add_eq_top
added theorem WithTop.add_lt_top
added theorem WithTop.add_ne_top
added theorem WithTop.add_top
added theorem WithTop.coe_add
added theorem WithTop.coe_addHom
added theorem WithTop.coe_eq_ofNat
added theorem WithTop.coe_natCast
added theorem WithTop.coe_nsmul
added theorem WithTop.coe_ofNat
added theorem WithTop.natCast_ne_top
added theorem WithTop.ofNat_eq_coe
added theorem WithTop.ofNat_ne_top
added theorem WithTop.top_add
added theorem WithTop.top_ne_natCast
added theorem WithTop.top_ne_ofNat
added theorem WithTop.zero_lt_coe
added theorem WithTop.zero_lt_top
added theorem add_top
added theorem top_add
deleted theorem add_top
deleted theorem top_add
deleted def WithBot.addHom
deleted theorem WithBot.add_bot
deleted theorem WithBot.add_eq_bot
deleted theorem WithBot.add_eq_coe
deleted theorem WithBot.add_left_cancel
deleted theorem WithBot.add_ne_bot
deleted theorem WithBot.add_right_cancel
deleted theorem WithBot.bot_add
deleted theorem WithBot.bot_lt_add
deleted theorem WithBot.bot_ne_natCast
deleted theorem WithBot.bot_ne_ofNat
deleted theorem WithBot.coe_add
deleted theorem WithBot.coe_addHom
deleted theorem WithBot.coe_eq_ofNat
deleted theorem WithBot.coe_natCast
deleted theorem WithBot.coe_nsmul
deleted theorem WithBot.coe_ofNat
deleted theorem WithBot.natCast_ne_bot
deleted theorem WithBot.ofNat_eq_coe
deleted theorem WithBot.ofNat_ne_bot
deleted def WithTop.addHom
deleted theorem WithTop.add_eq_coe
deleted theorem WithTop.add_eq_top
deleted theorem WithTop.add_left_cancel
deleted theorem WithTop.add_lt_top
deleted theorem WithTop.add_ne_top
deleted theorem WithTop.add_right_cancel
deleted theorem WithTop.add_top
deleted theorem WithTop.coe_add
deleted theorem WithTop.coe_addHom
deleted theorem WithTop.coe_eq_ofNat
deleted theorem WithTop.coe_natCast
deleted theorem WithTop.coe_nsmul
deleted theorem WithTop.coe_ofNat
deleted theorem WithTop.natCast_ne_top
deleted theorem WithTop.ofNat_eq_coe
deleted theorem WithTop.ofNat_ne_top
deleted theorem WithTop.top_add
deleted theorem WithTop.top_ne_natCast
deleted theorem WithTop.top_ne_ofNat
deleted theorem WithTop.zero_lt_coe
deleted theorem WithTop.zero_lt_top