Theorems · Theorem · linear algebra

Matrix.mul_single_eq_updateCol_zero

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (A : Matrix l m α) (i : m) (j : n) (r : α),
  A * Matrix.single i j r = Matrix.updateCol 0 j (MulOpposite.op r • A.col i)

Defined in

Mathlib.LinearAlgebra.Matrix.RowCol

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqFintypeNonUnitalNonAssocSemiring