add_monoid_hom.cod_restrict

Stream: Is there code for X?

[Markus Himmel]

In linear_algebra/basic.lean, we have

def cod_restrict (p : submodule R M) (f : M₂ →ₗ[R] M) (h : ∀c, f c ∈ p) : M₂ →ₗ[R] p :=
by refine {to_fun := λc, ⟨f c, h c⟩, ..}; intros; apply set_coe.ext; simp

Do we have the analogous definition for add_monoid_hom?