Documentation

Mathlib.LinearAlgebra.Matrix.Symmetric

Symmetric matrices #

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

Main definition #

Tags #

symm, symmetric, matrix

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

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

Equations
  • A.IsSymm = (A.transpose = A)
source
instance Matrix.instDecidableIsSymmOfEqTranspose {α : Type u_1} {n : Type u_3} (A : Matrix n n α) [Decidable (A.transpose = A)] :
Decidable A.IsSymm
Equations
source
theorem Matrix.IsSymm.eq {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) :
A.transpose = A
source
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.

source
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.

source
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
source
theorem Matrix.isSymm_mul_transpose_self {α : Type u_1} {n : Type u_3} [Fintype n] [CommSemiring α] (A : Matrix n n α) :
(A * A.transpose).IsSymm
source
theorem Matrix.isSymm_transpose_mul_self {α : Type u_1} {n : Type u_3} [Fintype n] [CommSemiring α] (A : Matrix n n α) :
(A.transpose * A).IsSymm
source
theorem Matrix.isSymm_add_transpose_self {α : Type u_1} {n : Type u_3} [AddCommSemigroup α] (A : Matrix n n α) :
(A + A.transpose).IsSymm
source
theorem Matrix.isSymm_transpose_add_self {α : Type u_1} {n : Type u_3} [AddCommSemigroup α] (A : Matrix n n α) :
(A.transpose + A).IsSymm
source
@[simp]
theorem Matrix.isSymm_zero {α : Type u_1} {n : Type u_3} [Zero α] :
Matrix.IsSymm 0
source
@[simp]
theorem Matrix.isSymm_one {α : Type u_1} {n : Type u_3} [DecidableEq n] [Zero α] [One α] :
Matrix.IsSymm 1
source
theorem Matrix.IsSymm.pow {α : Type u_1} {n : Type u_3} [CommSemiring α] [Fintype n] [DecidableEq n] {A : Matrix n n α} (h : A.IsSymm) (k : ℕ) :
(A ^ k).IsSymm
source
@[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
source
@[simp]
theorem Matrix.IsSymm.transpose {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) :
A.transpose.IsSymm
source
@[simp]
theorem Matrix.IsSymm.conjTranspose {α : Type u_1} {n : Type u_3} [Star α] {A : Matrix n n α} (h : A.IsSymm) :
A.conjTranspose.IsSymm
source
@[simp]
theorem Matrix.IsSymm.neg {α : Type u_1} {n : Type u_3} [Neg α] {A : Matrix n n α} (h : A.IsSymm) :
(-A).IsSymm
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem Matrix.IsSymm.submatrix {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (h : A.IsSymm) (f : m → n) :
(A.submatrix f f).IsSymm
source
@[simp]
theorem Matrix.isSymm_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [Zero α] (v : n → α) :
(Matrix.diagonal v).IsSymm

The diagonal matrix diagonal v is symmetric.

source
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) :
(Matrix.fromBlocks A B C D).IsSymm

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

source
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 α} :
(Matrix.fromBlocks A B C D).IsSymm ↔ A.IsSymm ∧ B.transpose = C ∧ C.transpose = B ∧ D.IsSymm

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