mathlib3

520bbe69 - feat(algebra/non_unital_alg_hom): define non_unital_alg_hom (#7863)

feat(algebra/non_unital_alg_hom): define non_unital_alg_hom (#7863) The motivation is to be able to state the universal property for a magma algebra using bundled morphisms.