Theorems · Theorem

Matrix.cons_vecMul_cons

∀ {α : Type u} {n : ℕ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (x : α) (v : Fin n → α) (w : o' → α)
  (B : Fin n → o' → α),
  Matrix.vecMul (Matrix.vecCons x v) (Matrix.of (Matrix.vecCons w B)) = x • w + Matrix.vecMul v (Matrix.of B)

Defined in

Mathlib.LinearAlgebra.Matrix.Notation

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiring