Commit 2022-04-26 02:57 4de65278

feat(algebra/ring/basic): define non-unital commutative (semi)rings (#13476) This adds the classes of non-unital commutative (semi)rings. These are necessary to talk about, for example, non-unital commutative C∗-algebras such as C₀(X, ℂ) which are vital for the continuous functional calculus. In addition, we weaken many type class assumptions in algebra/ring/basic to non_unital_non_assoc_ring.