Commit 2020-06-25 04:35 8f04a92a

refactor(algebra/*): small API fixes (#3157)

Changes to canonically_ordered_comm_semiring

• in the definition of canonically_ordered_comm_semiring replace mul_eq_zero_iff with eq_zero_or_eq_zero_of_mul_eq_zero; the other implication is always true because of [semiring];
• add instance canonically_ordered_comm_semiring.to_no_zero_divisors;

Changes to with_top

• use to_additive for with_top.has_one, with_top.coe_one etc;
• move with_top.coe_ne_zero to algebra.ordered_group;
• add with_top.has_add, make coe_add, coe_bit* require only [has_add α];
• use proper instances for lemmas about multiplication in with_top, not just canonically_ordered_comm_semiring for everything;

Changes to associates

• merge associates.mk_zero_eq and associates.mk_eq_zero_iff_eq_zero into associates.mk_eq_zero;
• drop associates.mul_zero, associates.zero_mul, associates.zero_ne_one, and associates.mul_eq_zero_iff in favor of typeclass instances;

Misc changes

• drop mul_eq_zero_iff_eq_zero_or_eq_zero in favor of mul_eq_zero;
• drop ennreal.mul_eq_zero in favor of mul_eq_zero from instance.