mathlib

4de65278 - feat(algebra/ring/basic): define non-unital commutative (semi)rings (#13476)

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`.