mathlib3

86bf83ab - feat(algebra/ring): mark a useful lemma simp and generalize unit neg lemmas (#16993)

feat(algebra/ring): mark a useful lemma simp and generalize unit neg lemmas (#16993) Mark the lemma that states `is_unit (-x) \iff is_unit x` as `simp`, and while we are here generalize a couple of typeclasses to a general monoid with some distributive negation.