Summing a single coordinate in a family of submodules

theorem Submodule.sum_coe_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (p : ι → Submodule R M) (i : ι) (x : ↥(p i)) : ∑ j : ι, ↑(Pi.single i x j) = ↑x

The ambient sum of a family supported in one submodule is its nonzero coordinate.