Theorems · Theorem · linear algebra

Matrix.vecMul_sum

∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {ι : Type u_14} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : Fintype n] (x : n → α) (s : Finset ι) (y : ι → Matrix n m α),
  Matrix.vecMul x (∑ i ∈ s, y i) = ∑ i ∈ s, Matrix.vecMul x (y i)

Defined in

Mathlib.Data.Matrix.Basic

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NonUnitalNonAssocSemiringFintype