Commit 2023-04-03 10:24 f1dea497

View on Github →

feat: port Data.Matrix.Hadamard (#3238)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Hadamard.lean

added theorem Matrix.add_hadamard

added theorem Matrix.diagonal_hadamard_diagonal

added theorem Matrix.dotProduct_vecMul_hadamard

added def Matrix.hadamard

added theorem Matrix.hadamard_add

added theorem Matrix.hadamard_apply

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