HepLean 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)
Instances For
    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.