Theorems · Theorem

Matrix.dotProduct_cons

∀ {α : Type u} {n : ℕ} [inst : AddCommMonoid α] [inst_1 : Mul α] (v : Fin n.succ → α) (x : α) (w : Fin n → α),
  v ⬝ᵥ Matrix.vecCons x w = Matrix.vecHead v * x + Matrix.vecTail v ⬝ᵥ w

Defined in

Mathlib.LinearAlgebra.Matrix.Notation

Cited by

5 results in Mathlib

Foundations

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

Assumes

AddCommMonoidMul