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_reducible]
    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 j : n) :
    A j i = A i j
    source
    theorem Matrix.isSymm_mul_transpose_self {α : Type u_1} {n : Type u_3} [Fintype n] [NonUnitalCommSemiring α] (A : Matrix n n α) :
    (A * A.transpose).IsSymm
    source
    theorem Matrix.isSymm_transpose_mul_self {α : Type u_1} {n : Type u_3} [Fintype n] [NonUnitalCommSemiring α] (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 α] :
    IsSymm 0
    source
    @[simp]
    theorem Matrix.isSymm_one {α : Type u_1} {n : Type u_3} [DecidableEq n] [Zero α] [One α] :
    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_map_iff {α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α} {f : α → β} (hf : Function.Injective f) :
    (A.map f).IsSymm ↔ A.IsSymm
    source
    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_transpose_iff {α : Type u_1} {n : Type u_3} {A : Matrix n n α} :
    A.transpose.IsSymm ↔ A.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_conjTranspose_iff {α : Type u_1} {n : Type u_3} [InvolutiveStar α] {A : Matrix n n α} :
    A.conjTranspose.IsSymm ↔ A.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_neg_iff {α : Type u_1} {n : Type u_3} [InvolutiveNeg α] {A : Matrix n n α} :
    (-A).IsSymm ↔ A.IsSymm
    source
    @[simp]
    theorem Matrix.IsSymm.add {α : Type u_1} {n : Type u_3} {A 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 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_smul_iff {α : Type u_1} {n : Type u_3} {R : Type u_5} [Monoid R] [MulAction R α] {A : Matrix n n α} (k : R) [Invertible k] :
    (k • A).IsSymm ↔ A.IsSymm
    source
    theorem Matrix.IsSymm.dotProduct_mulVec_comm {α : Type u_1} {n : Type u_3} [Fintype n] [NonUnitalCommSemiring α] {A : Matrix n n α} (hA : A.IsSymm) {x y : n → α} :
    x ⬝ᵥ A.mulVec y = y ⬝ᵥ A.mulVec x
    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
    theorem Matrix.IsSymm.reindex {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (h : A.IsSymm) (f : n ≃ m) :
    ((Matrix.reindex f f) A).IsSymm
    source
    theorem Matrix.isSymm_reindex_iff {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix n n α} (f : n ≃ m) :
    ((reindex f f) A).IsSymm ↔ A.IsSymm
    source
    @[simp]
    theorem Matrix.isSymm_diagonal {α : Type u_1} {n : Type u_3} [DecidableEq n] [Zero α] (v : n → α) :
    (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 α} :
    (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.

    source
    theorem Matrix.isSymm_comp_iff {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m (Matrix n n α)} :
    ((comp m m n n α) A).IsSymm ↔ A.transpose = A.map fun (x : Matrix n n α) => x.transpose
    source
    theorem Matrix.isSymm_comp_iff_forall {α : Type u_1} {n : Type u_3} {m : Type u_4} {A : Matrix m m (Matrix n n α)} :
    ((comp m m n n α) A).IsSymm ↔ ∀ (i j : m) (i' j' : n), A j i j' i' = A i j i' j'