Commit 2026-09-01 10:16 ea7d8e76

View on Github →

chore(Algebra/Order/Ring/WithTop): use to_dual (#42628) This PR uses to_dual on Ring-related declarations on WithTop/WithBot. Some lemmas and instances only existed for WithTop, so they have now been added for WithBot. The type class assumption for the ring instances have been weakened into a form that to_dual is happy with. It now only assumes [Subsingleton (AddUnits α)] instead of [PartialOrder α] [CanonicallyOrderedAdd α]. Some generic instances about CovariantClass were given a low priority because to_dual doesn't like them.

Estimated changes

deleted theorem WithBot.bot_lt_mul
deleted theorem WithBot.bot_mul'
deleted theorem WithBot.bot_mul
deleted theorem WithBot.bot_mul_bot
deleted theorem WithBot.coe_mul
deleted theorem WithBot.coe_mul_eq_bind
deleted theorem WithBot.coe_pow
deleted theorem WithBot.mul_bot'
deleted theorem WithBot.mul_bot
deleted theorem WithBot.mul_coe_eq_bind
deleted theorem WithBot.mul_def
deleted theorem WithBot.mul_eq_bot_iff
deleted theorem WithBot.mul_ne_bot
deleted theorem WithBot.unbotD_zero_mul
modified theorem WithTop.coe_mul
modified theorem WithTop.coe_pow
modified theorem WithTop.eq_top_of_pow
modified theorem WithTop.mul_top
modified theorem WithTop.pow_eq_top_iff
modified theorem WithTop.pow_lt_top_iff
modified theorem WithTop.pow_ne_top
modified theorem WithTop.top_mul
modified theorem WithTop.top_mul_top
modified theorem WithTop.top_pow