Theorems · Theorem · linear algebra

Matrix.vecMulVec_eq

∀ {m : Type u_2} {n : Type u_3} {α : Type v} (ι : Type u_6) [inst : Mul α] [inst_1 : AddCommMonoid α]
  [inst_2 : Unique ι] (w : m → α) (v : n → α), Matrix.vecMulVec w v = Matrix.replicateCol ι w * Matrix.replicateRow ι v

Defined in

Mathlib.LinearAlgebra.Matrix.RowCol

Cited by

7 results in Mathlib

Foundations

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

Assumes

MulAddCommMonoidUnique