mathlib3 documentation

linear_algebra.matrix.symmetric

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 #

Tags #

symm, symmetric, matrix

source
def matrix.is_symm {α : Type u_1} {n : Type u_3} (A : matrix n n α) :
Prop

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

Equations
source
theorem matrix.is_symm.eq {α : Type u_1} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) :
A.transpose = A
source
theorem matrix.is_symm.ext_iff {α : Type u_1} {n : Type u_3} {A : matrix n n α} :
A.is_symm ↔ ∀ (i j : n), A j i = A i j

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

source
@[ext]
theorem matrix.is_symm.ext {α : Type u_1} {n : Type u_3} {A : matrix n n α} :
(∀ (i j : n), A j i = A i j) → A.is_symm

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

source
theorem matrix.is_symm.apply {α : Type u_1} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) (i j : n) :
A j i = A i j
source
theorem matrix.is_symm_mul_transpose_self {α : Type u_1} {n : Type u_3} [fintype n] [comm_semiring α] (A : matrix n n α) :
(A.mul A.transpose).is_symm
source
theorem matrix.is_symm_transpose_mul_self {α : Type u_1} {n : Type u_3} [fintype n] [comm_semiring α] (A : matrix n n α) :
(A.transpose.mul A).is_symm
source
theorem matrix.is_symm_add_transpose_self {α : Type u_1} {n : Type u_3} [add_comm_semigroup α] (A : matrix n n α) :
(A + A.transpose).is_symm
source
theorem matrix.is_symm_transpose_add_self {α : Type u_1} {n : Type u_3} [add_comm_semigroup α] (A : matrix n n α) :
(A.transpose + A).is_symm
source
@[simp]
theorem matrix.is_symm_zero {α : Type u_1} {n : Type u_3} [has_zero α] :
0.is_symm
source
@[simp]
theorem matrix.is_symm_one {α : Type u_1} {n : Type u_3} [decidable_eq n] [has_zero α] [has_one α] :
1.is_symm
source
@[simp]
theorem matrix.is_symm.map {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) (f : α → β) :
(A.map f).is_symm
source
@[simp]
theorem matrix.is_symm.transpose {α : Type u_1} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) :
A.transpose.is_symm
source
@[simp]
theorem matrix.is_symm.conj_transpose {α : Type u_1} {n : Type u_3} [has_star α] {A : matrix n n α} (h : A.is_symm) :
A.conj_transpose.is_symm
source
@[simp]
theorem matrix.is_symm.neg {α : Type u_1} {n : Type u_3} [has_neg α] {A : matrix n n α} (h : A.is_symm) :
(-A).is_symm
source
@[simp]
theorem matrix.is_symm.add {α : Type u_1} {n : Type u_3} {A B : matrix n n α} [has_add α] (hA : A.is_symm) (hB : B.is_symm) :
(A + B).is_symm
source
@[simp]
theorem matrix.is_symm.sub {α : Type u_1} {n : Type u_3} {A B : matrix n n α} [has_sub α] (hA : A.is_symm) (hB : B.is_symm) :
(A - B).is_symm
source
@[simp]
theorem matrix.is_symm.smul {α : Type u_1} {n : Type u_3} {R : Type u_5} [has_smul R α] {A : matrix n n α} (h : A.is_symm) (k : R) :
(k • A).is_symm
source
@[simp]
theorem matrix.is_symm.submatrix {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : matrix n n α} (h : A.is_symm) (f : m → n) :
(A.submatrix f f).is_symm
source
@[simp]
theorem matrix.is_symm_diagonal {α : Type u_1} {n : Type u_3} [decidable_eq n] [has_zero α] (v : n → α) :
(matrix.diagonal v).is_symm

The diagonal matrix diagonal v is symmetric.

source
theorem matrix.is_symm.from_blocks {α : 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.is_symm) (hBC : B.transpose = C) (hD : D.is_symm) :
(matrix.from_blocks A B C D).is_symm

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

source
theorem matrix.is_symm_from_blocks_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.from_blocks A B C D).is_symm ↔ A.is_symm ∧ B.transpose = C ∧ C.transpose = B ∧ D.is_symm

This is the iff version of matrix.is_symm.from_blocks.