mathlib3

b77ff234 - feat(algebra/ring): add non-unital and non-associative rings (#12300)

feat(algebra/ring): add non-unital and non-associative rings (#12300) Following up on #11124. The longer term goal is to develop C^* algebras, where non-unital algebras are an essential part of the theory. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>