Commit 2023-05-18 11:07 7d0d674e

View on Github →

feat: port LinearAlgebra.Matrix.IsDiag (#4079)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/IsDiag.lean

added theorem Matrix.IsDiag.add

added theorem Matrix.IsDiag.conjTranspose

added theorem Matrix.IsDiag.diagonal_diag

added theorem Matrix.IsDiag.fromBlocks

added theorem Matrix.IsDiag.fromBlocks_of_isSymm

added theorem Matrix.IsDiag.isSymm

added theorem Matrix.IsDiag.kronecker

added theorem Matrix.IsDiag.map

added theorem Matrix.IsDiag.neg

added theorem Matrix.IsDiag.smul

added theorem Matrix.IsDiag.sub

added theorem Matrix.IsDiag.submatrix

added theorem Matrix.IsDiag.transpose

added def Matrix.IsDiag

added theorem Matrix.isDiag_conjTranspose_iff

added theorem Matrix.isDiag_diagonal

added theorem Matrix.isDiag_fromBlocks_iff

added theorem Matrix.isDiag_iff_diagonal_diag

added theorem Matrix.isDiag_neg_iff

added theorem Matrix.isDiag_of_subsingleton

added theorem Matrix.isDiag_one

added theorem Matrix.isDiag_smul_one

added theorem Matrix.isDiag_transpose_iff

added theorem Matrix.isDiag_zero

added theorem Matrix.mul_transpose_self_isDiag_iff_hasOrthogonalRows

added theorem Matrix.transpose_mul_self_isDiag_iff_hasOrthogonalCols