Commit 2026-01-31 00:21 47d7a528

View on Github →

feat(LinearAlgebra/Matrix/Hadamard): some API (#34600) Also move diagonal section earlier in file; change fun i => M i i to M.diag; and golf stuff using new results.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

added theorem Matrix.isAdjMatrix_iff_hadamard

Modified Mathlib/Data/Matrix/Diagonal.lean

added theorem Matrix.diagonal_zero'

Modified Mathlib/LinearAlgebra/Matrix/Hadamard.lean

added theorem Matrix.diagonal_hadamard

added theorem Matrix.diagonal_hadamard_eq_diagonal_iff

added theorem Matrix.hadamard_diagonal

added theorem Matrix.hadamard_diagonal_eq_diagonal_iff

added theorem Matrix.hadamard_of_one

modified theorem Matrix.hadamard_one

added theorem Matrix.hadamard_one_eq_diagonal_iff

added theorem Matrix.hadamard_one_eq_one_iff

added theorem Matrix.hadamard_one_eq_zero_iff

added theorem Matrix.hadamard_self_eq_self_iff

added theorem Matrix.of_one_hadamard

modified theorem Matrix.one_hadamard

added theorem Matrix.one_hadamard_eq_diagonal_iff

added theorem Matrix.one_hadamard_eq_one_iff

added theorem Matrix.one_hadamard_eq_zero_iff