Inserting a zero coordinate in a dependent family of modules

noncomputable def LinearMap.insertZeroCoordinate (R : Type u_1) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (a : ι) : ((i : { i : ι // i ≠ a }) → M ↑i) →ₗ[R] (i : ι) → M i

Extend a family on the complement of one index by zero at that index.

theorem LinearMap.insertZeroCoordinate_self (R : Type u_1) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (a : ι) (g : (i : { i : ι // i ≠ a }) → M ↑i) : (insertZeroCoordinate R M a) g a = 0

theorem LinearMap.insertZeroCoordinate_other (R : Type u_1) [Semiring R] {ι : Type u_2} (M : ι → Type u_3) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (a : ι) (g : (i : { i : ι // i ≠ a }) → M ↑i) (b : { i : ι // i ≠ a }) : (insertZeroCoordinate R M a) g ↑b = g b