Commit 2023-04-04 12:51 ecb79e44

View on Github →

feat: port LinearAlgebra.Matrix.Symmetric (#3258)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Symmetric.lean

added theorem Matrix.IsSymm.add

added theorem Matrix.IsSymm.apply

added theorem Matrix.IsSymm.conjTranspose

added theorem Matrix.IsSymm.eq

added theorem Matrix.IsSymm.ext

added theorem Matrix.IsSymm.ext_iff

added theorem Matrix.IsSymm.fromBlocks

added theorem Matrix.IsSymm.map

added theorem Matrix.IsSymm.neg

added theorem Matrix.IsSymm.smul

added theorem Matrix.IsSymm.sub

added theorem Matrix.IsSymm.submatrix

added theorem Matrix.IsSymm.transpose

added def Matrix.IsSymm

added theorem Matrix.isSymm_add_transpose_self

added theorem Matrix.isSymm_diagonal

added theorem Matrix.isSymm_fromBlocks_iff

added theorem Matrix.isSymm_mul_transpose_self

added theorem Matrix.isSymm_one

added theorem Matrix.isSymm_transpose_add_self

added theorem Matrix.isSymm_transpose_mul_self

added theorem Matrix.isSymm_zero