∀ {R : Type u_3} [inst : Semiring R] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_1} (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N)
  (h : ∀ (v : ι → M), f v ∈ p) [inst_5 : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
  ((↑f).codRestrict p h).toFun (Function.update m i (c • x)) = c • ((↑f).codRestrict p h).toFun (Function.update m i x)