# Symmetric matrices #

This file contains the definition and basic results about symmetric matrices.

## Main definition #

• Matrix.isSymm: a matrix A : Matrix n n α is "symmetric" if Aᵀ = A.

## Tags #

symm, symmetric, matrix

def Matrix.IsSymm {α : Type u_1} {n : Type u_3} (A : Matrix n n α) :

A matrix A : Matrix n n α is "symmetric" if Aᵀ = A.

Equations
• A.IsSymm = (A.transpose = A)
Instances For
instance Matrix.instDecidableIsSymmOfEqTranspose {α : Type u_1} {n : Type u_3} (A : Matrix n n α) [Decidable (A.transpose = A)] :
Decidable A.IsSymm
Equations
theorem Matrix.IsSymm.eq {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) :
A.transpose = A
theorem Matrix.IsSymm.ext_iff {α : Type u_1} {n : Type u_3} {A : Matrix n n α} :
A.IsSymm ∀ (i j : n), A j i = A i j

A version of Matrix.ext_iff that unfolds the Matrix.transpose.

theorem Matrix.IsSymm.ext {α : Type u_1} {n : Type u_3} {A : Matrix n n α} :
(∀ (i j : n), A j i = A i j)A.IsSymm

A version of Matrix.ext that unfolds the Matrix.transpose.

theorem Matrix.IsSymm.apply {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) (i : n) (j : n) :
A j i = A i j
theorem Matrix.isSymm_mul_transpose_self {α : Type u_1} {n : Type u_3} [] [] (A : Matrix n n α) :
(A * A.transpose).IsSymm
theorem Matrix.isSymm_transpose_mul_self {α : Type u_1} {n : Type u_3} [] [] (A : Matrix n n α) :
(A.transpose * A).IsSymm
theorem Matrix.isSymm_add_transpose_self {α : Type u_1} {n : Type u_3} [] (A : Matrix n n α) :
(A + A.transpose).IsSymm
theorem Matrix.isSymm_transpose_add_self {α : Type u_1} {n : Type u_3} [] (A : Matrix n n α) :
(A.transpose + A).IsSymm
@[simp]
theorem Matrix.isSymm_zero {α : Type u_1} {n : Type u_3} [Zero α] :
@[simp]
theorem Matrix.isSymm_one {α : Type u_1} {n : Type u_3} [] [Zero α] [One α] :
theorem Matrix.IsSymm.pow {α : Type u_1} {n : Type u_3} [] [] [] {A : Matrix n n α} (h : A.IsSymm) (k : ) :
(A ^ k).IsSymm
@[simp]
theorem Matrix.IsSymm.map {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) (f : αβ) :
(A.map f).IsSymm
@[simp]
theorem Matrix.IsSymm.transpose {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) :
A.transpose.IsSymm
@[simp]
theorem Matrix.IsSymm.conjTranspose {α : Type u_1} {n : Type u_3} [Star α] {A : Matrix n n α} (h : A.IsSymm) :
A.conjTranspose.IsSymm
@[simp]
theorem Matrix.IsSymm.neg {α : Type u_1} {n : Type u_3} [Neg α] {A : Matrix n n α} (h : A.IsSymm) :
(-A).IsSymm
@[simp]
theorem Matrix.IsSymm.add {α : Type u_1} {n : Type u_3} {A : Matrix n n α} {B : Matrix n n α} [Add α] (hA : A.IsSymm) (hB : B.IsSymm) :
(A + B).IsSymm
@[simp]
theorem Matrix.IsSymm.sub {α : Type u_1} {n : Type u_3} {A : Matrix n n α} {B : Matrix n n α} [Sub α] (hA : A.IsSymm) (hB : B.IsSymm) :
(A - B).IsSymm
@[simp]
theorem Matrix.IsSymm.smul {α : Type u_1} {n : Type u_3} {R : Type u_5} [SMul R α] {A : Matrix n n α} (h : A.IsSymm) (k : R) :
(k A).IsSymm
@[simp]
theorem Matrix.IsSymm.submatrix {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (h : A.IsSymm) (f : mn) :
(A.submatrix f f).IsSymm
@[simp]
theorem Matrix.isSymm_diagonal {α : Type u_1} {n : Type u_3} [] [Zero α] (v : nα) :
().IsSymm

The diagonal matrix diagonal v is symmetric.

theorem Matrix.IsSymm.fromBlocks {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} (hA : A.IsSymm) (hBC : B.transpose = C) (hD : D.IsSymm) :
(A.fromBlocks B C D).IsSymm

A block matrix A.fromBlocks B C D is symmetric, if A and D are symmetric and Bᵀ = C.

theorem Matrix.isSymm_fromBlocks_iff {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} :
(A.fromBlocks B C D).IsSymm A.IsSymm B.transpose = C C.transpose = B D.IsSymm

This is the iff version of Matrix.isSymm.fromBlocks.