Theorems · Theorem · linear algebra

Matrix.dotProduct_vecMul_hadamard

∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : NonUnitalSemiring α] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] (v : m → α) (w : n → α),
  Matrix.vecMul v (A.hadamard B) ⬝ᵥ w = (Matrix.diagonal v * A * (B * Matrix.diagonal w).transpose).trace

Defined in

Mathlib.LinearAlgebra.Matrix.Hadamard

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintypeNonUnitalSemiringDecidableEqDecidableEq