Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 05:56 a7be93b2

View on Github →

feat(data/matrix/hadamard): add the Hadamard product (#8956)

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.diagonal_conj_transpose

Created src/data/matrix/hadamard.lean

added theorem matrix.add_hadamard

added theorem matrix.diagonal_hadamard_diagonal

added theorem matrix.dot_product_vec_mul_hadamard

added def matrix.hadamard

added theorem matrix.hadamard_add

added theorem matrix.hadamard_assoc

added theorem matrix.hadamard_comm

added theorem matrix.hadamard_one

added theorem matrix.hadamard_smul

added theorem matrix.hadamard_zero

added theorem matrix.one_hadamard

added theorem matrix.smul_hadamard

added theorem matrix.sum_hadamard_eq

added theorem matrix.zero_hadamard