mathlib

23d61413 - chore(algebra/ring,char_zero): generalize some lemmas (#3141)

chore(algebra/ring,char_zero): generalize some lemmas (#3141) `mul_eq_zero` etc only need `[mul_zero_class]` and `[no_zero_divisors]`. In particular, they don't need `has_neg`. Also deduplicate with `group_with_zero.*`.