Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-14 08:41 790e98fb

View on Github →

feat(linear_algebra/matrix/is_diag): add a file (#9010)

Estimated changes

Created src/linear_algebra/matrix/is_diag.lean

added theorem matrix.is_diag.add

added theorem matrix.is_diag.conj_transpose

added theorem matrix.is_diag.exists_diagonal

added theorem matrix.is_diag.from_blocks

added theorem matrix.is_diag.from_blocks_of_is_symm

added theorem matrix.is_diag.is_symm

added theorem matrix.is_diag.kronecker

added theorem matrix.is_diag.map

added theorem matrix.is_diag.minor

added theorem matrix.is_diag.neg

added theorem matrix.is_diag.smul

added theorem matrix.is_diag.sub

added theorem matrix.is_diag.transpose

added def matrix.is_diag

added theorem matrix.is_diag_conj_transpose_iff

added theorem matrix.is_diag_diagonal

added theorem matrix.is_diag_from_blocks_iff

added theorem matrix.is_diag_iff_exists_diagonal

added theorem matrix.is_diag_neg_iff

added theorem matrix.is_diag_of_subsingleton

added theorem matrix.is_diag_one

added theorem matrix.is_diag_smul_one

added theorem matrix.is_diag_transpose_iff

added theorem matrix.is_diag_zero

added theorem matrix.mul_transpose_self_is_diag_iff_has_orthogonal_rows

added theorem matrix.transpose_mul_self_is_diag_iff_has_orthogonal_cols

Created src/linear_algebra/matrix/orthogonal.lean

added theorem matrix.has_orthogonal_cols.has_orthogonal_rows

added theorem matrix.has_orthogonal_cols.transpose_has_orthogonal_rows

added def matrix.has_orthogonal_cols

added theorem matrix.has_orthogonal_rows.has_orthogonal_cols

added theorem matrix.has_orthogonal_rows.transpose_has_orthogonal_cols

added def matrix.has_orthogonal_rows

added theorem matrix.transpose_has_orthogonal_cols_iff_has_orthogonal_rows

added theorem matrix.transpose_has_orthogonal_rows_iff_has_orthogonal_cols