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
Instances For
    source
    instance Matrix.instDecidableIsSymm {α : Type u_1} {n : Type u_3} (A : Matrix n n α) [Decidable (Matrix.transpose A = A)] :
    Decidable (Matrix.IsSymm A)
    Equations
    source
    theorem Matrix.IsSymm.eq {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : Matrix.IsSymm A) :
    Matrix.transpose A = A
    source
    theorem Matrix.IsSymm.ext_iff {α : Type u_1} {n : Type u_3} {A : Matrix n n α} :
    Matrix.IsSymm A ↔ ∀ (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) → Matrix.IsSymm A

    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 : Matrix.IsSymm A) (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 α) :
    Matrix.IsSymm (A * Matrix.transpose A)
    source
    theorem Matrix.isSymm_transpose_mul_self {α : Type u_1} {n : Type u_3} [Fintype n] [CommSemiring α] (A : Matrix n n α) :
    Matrix.IsSymm (Matrix.transpose A * A)
    source
    theorem Matrix.isSymm_add_transpose_self {α : Type u_1} {n : Type u_3} [AddCommSemigroup α] (A : Matrix n n α) :
    Matrix.IsSymm (A + Matrix.transpose A)
    source
    theorem Matrix.isSymm_transpose_add_self {α : Type u_1} {n : Type u_3} [AddCommSemigroup α] (A : Matrix n n α) :
    Matrix.IsSymm (Matrix.transpose A + A)
    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 : Matrix.IsSymm A) (k : ℕ) :
    Matrix.IsSymm (A ^ k)
    source
    @[simp]
    theorem Matrix.IsSymm.map {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α} (h : Matrix.IsSymm A) (f : α → β) :
    Matrix.IsSymm (Matrix.map A f)
    source
    @[simp]
    theorem Matrix.IsSymm.transpose {α : Type u_1} {n : Type u_3} {A : Matrix n n α} (h : Matrix.IsSymm A) :
    Matrix.IsSymm (Matrix.transpose A)
    source
    @[simp]
    theorem Matrix.IsSymm.conjTranspose {α : Type u_1} {n : Type u_3} [Star α] {A : Matrix n n α} (h : Matrix.IsSymm A) :
    Matrix.IsSymm (Matrix.conjTranspose A)
    source
    @[simp]
    theorem Matrix.IsSymm.neg {α : Type u_1} {n : Type u_3} [Neg α] {A : Matrix n n α} (h : Matrix.IsSymm A) :
    Matrix.IsSymm (-A)
    source
    @[simp]
    theorem Matrix.IsSymm.add {α : Type u_1} {n : Type u_3} {A : Matrix n n α} {B : Matrix n n α} [Add α] (hA : Matrix.IsSymm A) (hB : Matrix.IsSymm B) :
    Matrix.IsSymm (A + B)
    source
    @[simp]
    theorem Matrix.IsSymm.sub {α : Type u_1} {n : Type u_3} {A : Matrix n n α} {B : Matrix n n α} [Sub α] (hA : Matrix.IsSymm A) (hB : Matrix.IsSymm B) :
    Matrix.IsSymm (A - B)
    source
    @[simp]
    theorem Matrix.IsSymm.smul {α : Type u_1} {n : Type u_3} {R : Type u_5} [SMul R α] {A : Matrix n n α} (h : Matrix.IsSymm A) (k : R) :
    Matrix.IsSymm (k • A)
    source
    @[simp]
    theorem Matrix.IsSymm.submatrix {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (h : Matrix.IsSymm A) (f : m → n) :
    Matrix.IsSymm (Matrix.submatrix A f f)
    source
    @[simp]
    theorem Matrix.isSymm_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [Zero α] (v : n → α) :
    Matrix.IsSymm (Matrix.diagonal v)

    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 : Matrix.IsSymm A) (hBC : Matrix.transpose B = C) (hD : Matrix.IsSymm D) :
    Matrix.IsSymm (Matrix.fromBlocks A B C D)

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

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