mathlib3

7edb6d5d - refactor(algebra/field/basic): generalize some lemmas to division monoids (#15845)

refactor(algebra/field/basic): generalize some lemmas to division monoids (#15845) Generalize various lemmas about the relation of division and negation from `division_ring` to any `division_monoid` with `has_distrib_neg`. This permits these lemmas to apply to `units K` where `ring K`, and to `sign_type`.