Symmetric matrices #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains the definition and basic results about symmetric matrices.
Main definition #
symm, symmetric, matrix
A : matrix n n α is "symmetric" if
Aᵀ = A.
The diagonal matrix
diagonal v is symmetric.
A block matrix
A.from_blocks B C D is symmetric,
D are symmetric and
Bᵀ = C.