mathlib

ef7aa94e - feat(algebra/ring/basic): define non-unital, non-associative rings (#6786)

feat(algebra/ring/basic): define non-unital, non-associative rings (#6786) This introduces the following typeclasses beneath `semiring`: * `non_unital_non_assoc_semiring` * `non_unital_semiring` * `non_assoc_semiring` The goal is to use these to support a non-unital, non-associative algebras. The typeclass requirements of `subring`, `subsemiring`, and `ring_hom` are relaxed from `semiring` to `non_assoc_semiring`. Instances of these new typeclasses are added for: * alias types: * `opposite` * `ulift` * convolutive types: * `(add_)monoid_algebra` * `direct_sum` * `set_semiring` * `hahn_series` * elementwise types: * `locally_constant` * `pi` * `prod` * `finsupp` Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>