# Hadamard product of matrices #

This file defines the Hadamard product `Matrix.hadamard` and contains basic properties about them.

## Main definition #

- `Matrix.hadamard`: defines the Hadamard product, which is the pointwise product of two matrices of the same size.

## Notation #

- `⊙`: the Hadamard product `Matrix.hadamard`;

## References #

- https://en.wikipedia.org/wiki/hadamard_product_(matrices)

## Tags #

hadamard product, hadamard

source
def Matrix.hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] (A B : Matrix m n α) :
Matrix m n α

`Matrix.hadamard` (denoted as `⊙` within the Matrix namespace) defines the Hadamard product, which is the pointwise product of two matrices of the same size.

Equations

- A.hadamard B = Matrix.of fun (i : m) (j : n) => A i j * B i j

Instances For

source
@[simp]
theorem Matrix.hadamard_apply {α : Type u_1} {m : Type u_2} {n : Type u_3} [Mul α] (A B : Matrix m n α) (i : m) (j : n) :
A.hadamard B i j = A i j * B i j
source
def Matrix.«term_⊙_» :
Lean.TrailingParserDescr

`Matrix.hadamard` (denoted as `⊙` within the Matrix namespace) defines the Hadamard product, which is the pointwise product of two matrices of the same size.

Equations

- Matrix.«term_⊙_» = Lean.ParserDescr.trailingNode `Matrix.«term_⊙_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊙ ") (Lean.ParserDescr.cat `term 101))

Instances For

source
theorem Matrix.hadamard_comm {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [CommMagma α] :
A.hadamard B = B.hadamard A
source
theorem Matrix.hadamard_assoc {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [Semigroup α] :
(A.hadamard B).hadamard C = A.hadamard (B.hadamard C)
source
theorem Matrix.hadamard_add {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [Distrib α] :
A.hadamard (B + C) = A.hadamard B + A.hadamard C
source
theorem Matrix.add_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B C : Matrix m n α) [Distrib α] :
(B + C).hadamard A = B.hadamard A + C.hadamard A
source
@[simp]
theorem Matrix.smul_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [Mul α] [SMul R α] [IsScalarTower R α α] (k : R) :
(k • A).hadamard B = k • A.hadamard B
source
@[simp]
theorem Matrix.hadamard_smul {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_4} (A B : Matrix m n α) [Mul α] [SMul R α] [SMulCommClass R α α] (k : R) :
A.hadamard (k • B) = k • A.hadamard B
source
@[simp]
theorem Matrix.hadamard_zero {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [MulZeroClass α] :
A.hadamard 0 = 0
source
@[simp]
theorem Matrix.zero_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} (A : Matrix m n α) [MulZeroClass α] :
hadamard 0 A = 0
source
theorem Matrix.hadamard_one {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
M.hadamard 1 = diagonal fun (i : n) => M i i
source
theorem Matrix.one_hadamard {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroOneClass α] (M : Matrix n n α) :
hadamard 1 M = diagonal fun (i : n) => M i i
source
theorem Matrix.single_hadamard_single_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] (i : m) (j : n) (a b : α) :
(single i j a).hadamard (single i j b) = single i j (a * b)
source
@[deprecated Matrix.single_hadamard_single_eq (since := "2025-05-05")]
theorem Matrix.stdBasisMatrix_hadamard_stdBasisMatrix_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] (i : m) (j : n) (a b : α) :
(single i j a).hadamard (single i j b) = single i j (a * b)

Alias of `Matrix.single_hadamard_single_eq`.

source
theorem Matrix.single_hadamard_single_of_ne {α : Type u_1} {m : Type u_2} {n : Type u_3} [DecidableEq m] [DecidableEq n] [MulZeroClass α] {ia : m} {ja : n} {ib : m} {jb : n} (h : ¬(ia = ib ∧ ja = jb)) (a b : α) :
(single ia ja a).hadamard (single ib jb b) = 0
source
theorem Matrix.diagonal_hadamard_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [MulZeroClass α] (v w : n → α) :
(diagonal v).hadamard (diagonal w) = diagonal (v * w)
source
theorem Matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] :
∑ i : m, ∑ j : n, A.hadamard B i j = (A * B.transpose).trace
source
theorem Matrix.dotProduct_vecMul_hadamard {α : Type u_1} {m : Type u_2} {n : Type u_3} (A B : Matrix m n α) [Fintype m] [Fintype n] [Semiring α] [DecidableEq m] [DecidableEq n] (v : m → α) (w : n → α) :
vecMul v (A.hadamard B) ⬝ᵥ w = (diagonal v * A * (B * diagonal w).transpose).trace