Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-04 15:15 a4df4609

View on Github →

feat(linear_algebra/matrix/symmetric): add a file (#8955)

Estimated changes

Modified src/data/matrix/basic.lean

modified theorem matrix.transpose_smul

modified theorem matrix.transpose_sub

Created src/linear_algebra/matrix/symmetric.lean

added theorem matrix.is_symm.add

added theorem matrix.is_symm.apply

added theorem matrix.is_symm.conj_transpose

added theorem matrix.is_symm.eq

added theorem matrix.is_symm.ext

added theorem matrix.is_symm.ext_iff

added theorem matrix.is_symm.from_blocks

added theorem matrix.is_symm.map

added theorem matrix.is_symm.minor

added theorem matrix.is_symm.neg

added theorem matrix.is_symm.smul

added theorem matrix.is_symm.sub

added theorem matrix.is_symm.transpose

added def matrix.is_symm

added theorem matrix.is_symm_add_transpose_self

added theorem matrix.is_symm_diagonal

added theorem matrix.is_symm_from_blocks_iff

added theorem matrix.is_symm_mul_transpose_self

added theorem matrix.is_symm_one

added theorem matrix.is_symm_transpose_add_self

added theorem matrix.is_symm_transpose_mul_self

added theorem matrix.is_symm_zero