mathlib

ece3044a - feat(algebra/ring/{pi, prod, opposite}): add basic defs for non_unital_ring_hom (#13958)

feat(algebra/ring/{pi, prod, opposite}): add basic defs for non_unital_ring_hom (#13958) The defs added mimic the corresponding ones for `ring_hom`, wherever possible. - [x] depends on: #13956 Co-authored-by: Oliver Nash <github@olivernash.org>