Zulip Chat Archive

Stream: Is there code for X?

Topic: add_monoid_hom.cod_restrict

view this post on Zulip Markus Himmel (Jul 04 2020 at 19:27):

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?

Last updated: May 16 2021 at 05:21 UTC