Theorems · Theorem · linear algebra

Matrix.mul_updateCol

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Fintype m]
  [inst_2 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (B : Matrix m n α) (j : n) (c : m → α),
  A * B.updateCol j c = (A * B).updateCol j (A.mulVec c)

Defined in

Mathlib.LinearAlgebra.Matrix.RowCol

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeNonUnitalNonAssocSemiring