Commit 2022-10-15 13:04 86bf83ab

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.