∀ {α : Type u_2} {M : Type u_1} (R : Type u_3) [inst : Fintype α] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (v : α → M) (f g : α → R), ∑ i, (f + g) i • v i = ∑ i, f i • v i + ∑ i, g i • v i