mathlib3
b72d2ab2 - feat(algebra/ring/basic): Introduce non-unital, non-associative rings (#11124)

Commit
4 years ago
feat(algebra/ring/basic): Introduce non-unital, non-associative rings (#11124) Adds the class `non_unital_non_assoc_ring` to `algebra.ring.basic` to represent rings which are not assumed to be unital or associative and shows that (unital, associative) rings are instances of `non_unital_non_assoc_ring`. Needed by #11073. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Author
Parents
Loading