Commit 2022-04-22 08:34 3d24b093

feat(algebra/ring/basic): define non-unital ring homs (#13430) This defines a new bundled hom type and associated class for non-unital (even non-associative) (semi)rings. The associated notation introduced for these homs is α →ₙ+* β to parallel the ring_hom notation α →+* β, where ₙ stands for "non-unital".