Commit 2024-07-17 15:24 ab9dec5b

View on Github →

chore (Algebra.Order.WithTop): split into unbundled and bundled (#14531) Much of the results in Algebra.Order.Monoid.WithTop only depend on unbundled ordered algebra instance parameters. We split those results out into a new file Algera.Order.Monoid.Unbundled.WithTop leaving the facts about bundled ordered monoids.

Estimated changes

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
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.bot_ne_one
added theorem WithBot.coe_add
added theorem WithBot.coe_addHom
added theorem WithBot.coe_eq_ofNat
added theorem WithBot.coe_eq_one
added theorem WithBot.coe_le_one
added theorem WithBot.coe_lt_one
added theorem WithBot.coe_natCast
added theorem WithBot.coe_nsmul
added theorem WithBot.coe_ofNat
added theorem WithBot.coe_one
added theorem WithBot.natCast_ne_bot
added theorem WithBot.ofNat_eq_coe
added theorem WithBot.ofNat_ne_bot
added theorem WithBot.one_eq_coe
added theorem WithBot.one_le_coe
added theorem WithBot.one_lt_coe
added theorem WithBot.one_ne_bot
added theorem WithBot.unbot_one'
added theorem WithBot.unbot_one
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_eq_one
added theorem WithTop.coe_le_one
added theorem WithTop.coe_lt_one
added theorem WithTop.coe_natCast
added theorem WithTop.coe_nsmul
added theorem WithTop.coe_ofNat
added theorem WithTop.coe_one
added theorem WithTop.natCast_ne_top
added theorem WithTop.ofNat_eq_coe
added theorem WithTop.ofNat_ne_top
added theorem WithTop.one_eq_coe
added theorem WithTop.one_le_coe
added theorem WithTop.one_lt_coe
added theorem WithTop.one_ne_top
added theorem WithTop.top_add
added theorem WithTop.top_ne_natCast
added theorem WithTop.top_ne_ofNat
added theorem WithTop.top_ne_one
added theorem WithTop.untop_one'
added theorem WithTop.untop_one
added theorem WithTop.zero_lt_coe
added theorem WithTop.zero_lt_top
deleted theorem WithBot.bot_ne_one
deleted theorem WithBot.coe_eq_one
deleted theorem WithBot.coe_le_one
deleted theorem WithBot.coe_lt_one
deleted theorem WithBot.coe_one
deleted theorem WithBot.one_eq_coe
deleted theorem WithBot.one_le_coe
deleted theorem WithBot.one_lt_coe
deleted theorem WithBot.one_ne_bot
deleted theorem WithBot.unbot_one'
deleted theorem WithBot.unbot_one
deleted theorem WithTop.coe_eq_one
deleted theorem WithTop.coe_le_one
deleted theorem WithTop.coe_lt_one
deleted theorem WithTop.coe_one
deleted theorem WithTop.one_eq_coe
deleted theorem WithTop.one_le_coe
deleted theorem WithTop.one_lt_coe
deleted theorem WithTop.one_ne_top
deleted theorem WithTop.top_ne_one
deleted theorem WithTop.untop_one'
deleted theorem WithTop.untop_one