Theorems · Theorem

Matrix.cons_dotProduct_cons

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

Defined in

Mathlib.LinearAlgebra.Matrix.Notation

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddCommMonoidMul