Commit 2021-08-02 12:31 c8b7816d

feat(algebra/ordered_monoid): add_eq_bot_iff (#8474) bot addition is saturating on the bottom. On the way, typeclass arguments were relaxed to just [add_semigroup α], and helper simp lemmas added for bot. The iff lemma added (add_eq_bot) is not exactly according to the naming convention, but matches the top lemma and related ones in the naming style, so the style is kept consistent. There is an API proof available, but the defeq proof (using the top equivalent) was used based on suggestions.