# 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;

## Tags #

def Matrix.hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} [Mul α] (A : Matrix m n α) (B : Matrix m n α) :
Matrix m n α

Matrix.hadamard 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
@[simp]
theorem Matrix.hadamard_apply {α : Type u_1} {m : Type u_4} {n : Type u_5} [Mul α] (A : Matrix m n α) (B : Matrix m n α) (i : m) (j : n) :
A.hadamard B i j = A i j * B i j
Equations
Instances For
theorem Matrix.hadamard_comm {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) [] :
theorem Matrix.hadamard_assoc {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [] :
theorem Matrix.hadamard_add {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [] :
theorem Matrix.add_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) (B : Matrix m n α) (C : Matrix m n α) [] :
@[simp]
theorem Matrix.smul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [] (k : R) :
@[simp]
theorem Matrix.hadamard_smul {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A : Matrix m n α) (B : Matrix m n α) [Mul α] [SMul R α] [] (k : R) :
@[simp]
theorem Matrix.hadamard_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : Matrix m n α) [] :