mathlib documentation

data.matrix.hadamard

Hadamard product of matrices #

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

Main definition #

Notation #

References #

Tags #

hadamard product, hadamard

@[simp]
def matrix.hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} [has_mul α] (A 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 B) i j = (A i j) * B i j
theorem matrix.hadamard_comm {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B : matrix m n α) [comm_semigroup α] :
A B = B A
theorem matrix.hadamard_assoc {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [semigroup α] :
A B C = A (B C)
theorem matrix.hadamard_add {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [distrib α] :
A (B + C) = A B + A C
theorem matrix.add_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A B C : matrix m n α) [distrib α] :
(B + C) A = B A + C A
@[simp]
theorem matrix.smul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A B : matrix m n α) [has_mul α] [has_scalar R α] [is_scalar_tower R α α] (k : R) :
(k A) B = k A B
@[simp]
theorem matrix.hadamard_smul {α : Type u_1} {m : Type u_4} {n : Type u_5} {R : Type u_6} (A B : matrix m n α) [has_mul α] [has_scalar R α] [smul_comm_class R α α] (k : R) :
A (k B) = k A B
@[simp]
theorem matrix.hadamard_zero {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : matrix m n α) [mul_zero_class α] :
A 0 = 0
@[simp]
theorem matrix.zero_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (A : matrix m n α) [mul_zero_class α] :
0 A = 0
theorem matrix.hadamard_one {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_one_class α] (M : matrix n n α) :
M 1 = matrix.diagonal (λ (i : n), M i i)
theorem matrix.one_hadamard {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_one_class α] (M : matrix n n α) :
1 M = matrix.diagonal (λ (i : n), M i i)
theorem matrix.diagonal_hadamard_diagonal {α : Type u_1} {n : Type u_5} [decidable_eq n] [mul_zero_class α] (v w : n → α) :
theorem matrix.sum_hadamard_eq {α : Type u_1} {m : Type u_4} {n : Type u_5} (R : Type u_6) (A B : matrix m n α) [fintype m] [fintype n] [semiring α] [semiring R] [module R α] :
∑ (i : m) (j : n), (A B) i j = (matrix.trace m R α) (A B)
theorem matrix.dot_product_vec_mul_hadamard {α : Type u_1} {m : Type u_4} {n : Type u_5} (R : Type u_6) (A B : matrix m n α) [fintype m] [fintype n] [semiring α] [semiring R] [module R α] [decidable_eq m] [decidable_eq n] (v : m → α) (w : n → α) :