Theorems · Theorem · linear algebra

Matrix.sum_apply

∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddCommMonoid α] (i : m) (j : n) (s : Finset β)
  (g : β → Matrix m n α), (∑ c ∈ s, g c) i j = ∑ c ∈ s, g c i j

Defined in

Mathlib.Data.Matrix.Basic

Cited by

9 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext, Quot.sound

Assumes

AddCommMonoid