Theorems · Theorem · linear algebra

Matrix.updateRow_zero_mul_updateCol_zero

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq l] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (i : l) (r : m → α) (j : n) (c : m → α),
  Matrix.updateRow 0 i r * Matrix.updateCol 0 j c = Matrix.single i j (r ⬝ᵥ c)

Defined in

Mathlib.LinearAlgebra.Matrix.RowCol

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqFintypeNonUnitalNonAssocSemiring