mathlib documentation

linear_algebra.matrix.symmetric

Symmetric matrices #

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

Main definition #

Tags #

symm, symmetric, matrix

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
theorem matrix.is_symm.eq {α : Type u_1} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) :
A = A
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.

@[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.

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
theorem matrix.is_symm_mul_transpose_self {α : Type u_1} {n : Type u_3} [fintype n] [comm_semiring α] (A : matrix n n α) :
theorem matrix.is_symm_transpose_mul_self {α : Type u_1} {n : Type u_3} [fintype n] [comm_semiring α] (A : matrix n n α) :
theorem matrix.is_symm_add_transpose_self {α : Type u_1} {n : Type u_3} [add_comm_semigroup α] (A : matrix n n α) :
theorem matrix.is_symm_transpose_add_self {α : Type u_1} {n : Type u_3} [add_comm_semigroup α] (A : matrix n n α) :
@[simp]
theorem matrix.is_symm_zero {α : Type u_1} {n : Type u_3} [has_zero α] :
@[simp]
theorem matrix.is_symm_one {α : Type u_1} {n : Type u_3} [decidable_eq n] [has_zero α] [has_one α] :
@[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
@[simp]
theorem matrix.is_symm.transpose {α : Type u_1} {n : Type u_3} {A : matrix n n α} (h : A.is_symm) :
@[simp]
theorem matrix.is_symm.conj_transpose {α : Type u_1} {n : Type u_3} [has_star α] {A : matrix n n α} (h : A.is_symm) :
@[simp]
theorem matrix.is_symm.neg {α : Type u_1} {n : Type u_3} [has_neg α] {A : matrix n n α} (h : A.is_symm) :
@[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
@[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
@[simp]
theorem matrix.is_symm.smul {α : Type u_1} {n : Type u_3} {R : Type u_5} [has_scalar R α] {A : matrix n n α} (h : A.is_symm) (k : R) :
(k A).is_symm
@[simp]
theorem matrix.is_symm.minor {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : matrix n n α} (h : A.is_symm) (f : m → n) :
(A.minor f f).is_symm
@[simp]
theorem matrix.is_symm_diagonal {α : Type u_1} {n : Type u_3} [decidable_eq n] [has_zero α] (v : n → α) :

The diagonal matrix diagonal v is symmetric.

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 = C) (hD : D.is_symm) :

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

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 α} :

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