Diagonal matrices #

This file defines diagonal matrices and the AddCommMonoidWithOne structure on matrices.

Main definitions #

Matrix.diagonal d: matrix with the vector d along the diagonal
Matrix.diag M: the diagonal of a square matrix
Matrix.instAddCommMonoidWithOne: matrices are an additive commutative monoid with one

source

def Matrix.diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) :

Matrix n n α

diagonal d is the square matrix such that (diagonal d) i i = d i and (diagonal d) i j = 0 if i ≠ j.

Note that bundled versions exist as:

Matrix.diagonalAddMonoidHom
Matrix.diagonalLinearMap
Matrix.diagonalRingHom
Matrix.diagonalAlgHom

Equations

Matrix.diagonal d = Matrix.of fun (i j : n) => if i = j then d i else 0

Instances For

source

theorem Matrix.diagonal_apply {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) (i j : n) :

Matrix.diagonal d i j = if i = j then d i else 0

source

@[simp]

theorem Matrix.diagonal_apply_eq {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) (i : n) :

Matrix.diagonal d i i = d i

source

@[simp]

theorem Matrix.diagonal_apply_ne {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) {i j : n} (h : i ≠ j) :

Matrix.diagonal d i j = 0

source

theorem Matrix.diagonal_apply_ne' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (d : n → α) {i j : n} (h : j ≠ i) :

Matrix.diagonal d i j = 0

source

@[simp]

theorem Matrix.diagonal_eq_diagonal_iff {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] {d₁ d₂ : n → α} :

Matrix.diagonal d₁ = Matrix.diagonal d₂ ↔ ∀ (i : n), d₁ i = d₂ i

source

theorem Matrix.diagonal_injective {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] :

Function.Injective Matrix.diagonal

source

@[simp]

theorem Matrix.diagonal_zero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] :

(Matrix.diagonal fun (x : n) => 0) = 0

source

@[simp]

theorem Matrix.diagonal_transpose {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (v : n → α) :

(Matrix.diagonal v).transpose = Matrix.diagonal v

source

@[simp]

theorem Matrix.diagonal_add {n : Type u_3} {α : Type v} [DecidableEq n] [AddZeroClass α] (d₁ d₂ : n → α) :

Matrix.diagonal d₁ + Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i + d₂ i

source

@[simp]

theorem Matrix.diagonal_smul {n : Type u_3} {R : Type u_7} {α : Type v} [DecidableEq n] [Zero α] [SMulZeroClass R α] (r : R) (d : n → α) :

Matrix.diagonal (r • d) = r • Matrix.diagonal d

source

@[simp]

theorem Matrix.diagonal_neg {n : Type u_3} {α : Type v} [DecidableEq n] [NegZeroClass α] (d : n → α) :

-Matrix.diagonal d = Matrix.diagonal fun (i : n) => -d i

source

@[simp]

theorem Matrix.diagonal_sub {n : Type u_3} {α : Type v} [DecidableEq n] [SubNegZeroMonoid α] (d₁ d₂ : n → α) :

Matrix.diagonal d₁ - Matrix.diagonal d₂ = Matrix.diagonal fun (i : n) => d₁ i - d₂ i

source

instance Matrix.instNatCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] :

NatCast (Matrix n n α)

Equations

Matrix.instNatCastOfZero = { natCast := fun (m : ℕ) => Matrix.diagonal fun (x : n) => ↑m }

source

theorem Matrix.diagonal_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) :

(Matrix.diagonal fun (x : n) => ↑m) = ↑m

source

theorem Matrix.diagonal_natCast' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) :

Matrix.diagonal ↑m = ↑m

source

theorem Matrix.diagonal_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :

(Matrix.diagonal fun (x : n) => OfNat.ofNat m) = OfNat.ofNat m

source

theorem Matrix.diagonal_ofNat' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :

Matrix.diagonal (OfNat.ofNat m) = OfNat.ofNat m

source

instance Matrix.instIntCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] :

IntCast (Matrix n n α)

Equations

Matrix.instIntCastOfZero = { intCast := fun (m : ℤ) => Matrix.diagonal fun (x : n) => ↑m }

source

theorem Matrix.diagonal_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] (m : ℤ) :

(Matrix.diagonal fun (x : n) => ↑m) = ↑m

source

theorem Matrix.diagonal_intCast' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] (m : ℤ) :

Matrix.diagonal ↑m = ↑m

source

@[simp]

theorem Matrix.diagonal_map {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :

(Matrix.diagonal d).map f = Matrix.diagonal fun (m : n) => f (d m)

source

theorem Matrix.map_natCast {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [AddMonoidWithOne β] {f : α → β} (h : f 0 = 0) (d : ℕ) :

(↑d).map f = Matrix.diagonal fun (x : n) => f ↑d

source

theorem Matrix.map_ofNat {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [AddMonoidWithOne β] {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] :

(OfNat.ofNat d).map f = Matrix.diagonal fun (x : n) => f (OfNat.ofNat d)

source

theorem Matrix.map_intCast {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddGroupWithOne α] [AddGroupWithOne β] {f : α → β} (h : f 0 = 0) (d : ℤ) :

(↑d).map f = Matrix.diagonal fun (x : n) => f ↑d

source

theorem Matrix.diagonal_unique {m : Type u_2} {α : Type v} [Unique m] [DecidableEq m] [Zero α] (d : m → α) :

Matrix.diagonal d = Matrix.of fun (x x : m) => d default

source

instance Matrix.one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :

One (Matrix n n α)

Equations

Matrix.one = { one := Matrix.diagonal fun (x : n) => 1 }

source

@[simp]

theorem Matrix.diagonal_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :

(Matrix.diagonal fun (x : n) => 1) = 1

source

theorem Matrix.one_apply {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i j : n} :

1 i j = if i = j then 1 else 0

source

@[simp]

theorem Matrix.one_apply_eq {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] (i : n) :

1 i i = 1

source

@[simp]

theorem Matrix.one_apply_ne {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i j : n} :

i ≠ j → 1 i j = 0

source

theorem Matrix.one_apply_ne' {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i j : n} :

j ≠ i → 1 i j = 0

source

@[simp]

theorem Matrix.map_one {n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [One α] [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :

Matrix.map 1 f = 1

source

theorem Matrix.one_eq_pi_single {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {i j : n} :

1 i j = Pi.single i 1 j

source

instance Matrix.instAddMonoidWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] :

AddMonoidWithOne (Matrix n n α)

Equations

Matrix.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

source

instance Matrix.instAddGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] :

AddGroupWithOne (Matrix n n α)

Equations

Matrix.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

instance Matrix.instAddCommMonoidWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommMonoidWithOne α] :

AddCommMonoidWithOne (Matrix n n α)

Equations

Matrix.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

source

instance Matrix.instAddCommGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommGroupWithOne α] :

AddCommGroupWithOne (Matrix n n α)

Equations

Matrix.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

source

def Matrix.diag {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) :

The diagonal of a square matrix.

Equations

A.diag i = A i i

Instances For

source

@[simp]

theorem Matrix.diag_apply {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) :

A.diag i = A i i

source

@[simp]

theorem Matrix.diag_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] (a : n → α) :

(Matrix.diagonal a).diag = a

source

@[simp]

theorem Matrix.diag_transpose {n : Type u_3} {α : Type v} (A : Matrix n n α) :

A.transpose.diag = A.diag

source

@[simp]

theorem Matrix.diag_zero {n : Type u_3} {α : Type v} [Zero α] :

Matrix.diag 0 = 0

source

@[simp]

theorem Matrix.diag_add {n : Type u_3} {α : Type v} [Add α] (A B : Matrix n n α) :

(A + B).diag = A.diag + B.diag

source

@[simp]

theorem Matrix.diag_sub {n : Type u_3} {α : Type v} [Sub α] (A B : Matrix n n α) :

(A - B).diag = A.diag - B.diag

source

@[simp]

theorem Matrix.diag_neg {n : Type u_3} {α : Type v} [Neg α] (A : Matrix n n α) :

(-A).diag = -A.diag

source

@[simp]

theorem Matrix.diag_smul {n : Type u_3} {R : Type u_7} {α : Type v} [SMul R α] (r : R) (A : Matrix n n α) :

(r • A).diag = r • A.diag

source

@[simp]

theorem Matrix.diag_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :

Matrix.diag 1 = 1

source

theorem Matrix.diag_map {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : Matrix n n α} :

(A.map f).diag = f ∘ A.diag

source

@[simp]

theorem Matrix.transpose_eq_diagonal {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] {M : Matrix n n α} {v : n → α} :

M.transpose = Matrix.diagonal v ↔ M = Matrix.diagonal v

source

@[simp]

theorem Matrix.transpose_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :

Matrix.transpose 1 = 1

source

@[simp]

theorem Matrix.transpose_eq_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] {M : Matrix n n α} :

M.transpose = 1 ↔ M = 1

source

@[simp]

theorem Matrix.transpose_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) :

(↑d).transpose = ↑d

source

@[simp]

theorem Matrix.transpose_eq_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} :

M.transpose = ↑d ↔ M = ↑d

source

@[simp]

theorem Matrix.transpose_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] :

(OfNat.ofNat d).transpose = OfNat.ofNat d

source

@[simp]

theorem Matrix.transpose_eq_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :

M.transpose = OfNat.ofNat d ↔ M = OfNat.ofNat d

source

@[simp]

theorem Matrix.transpose_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] (d : ℤ) :

(↑d).transpose = ↑d

source

@[simp]

theorem Matrix.transpose_eq_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] {M : Matrix n n α} {d : ℤ} :

M.transpose = ↑d ↔ M = ↑d

source

theorem Matrix.submatrix_diagonal {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l → m) (he : Function.Injective e) :

(Matrix.diagonal d).submatrix e e = Matrix.diagonal (d ∘ e)

Given a (m × m) diagonal matrix defined by a map d : m → α, if the reindexing map e is injective, then the resulting matrix is again diagonal.

source

theorem Matrix.submatrix_one {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l → m) (he : Function.Injective e) :

Matrix.submatrix 1 e e = 1

source

theorem Matrix.diag_submatrix {l : Type u_1} {m : Type u_2} {α : Type v} (A : Matrix m m α) (e : l → m) :

(A.submatrix e e).diag = A.diag ∘ e

simp lemmas for Matrix.submatrixs interaction with Matrix.diagonal, 1, and Matrix.mul for when the mappings are bundled.

source

@[simp]

theorem Matrix.submatrix_diagonal_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ↪ m) :

(Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)

source

@[simp]

theorem Matrix.submatrix_diagonal_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [DecidableEq m] [DecidableEq l] (d : m → α) (e : l ≃ m) :

(Matrix.diagonal d).submatrix ⇑e ⇑e = Matrix.diagonal (d ∘ ⇑e)

source

@[simp]

theorem Matrix.submatrix_one_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) :

Matrix.submatrix 1 ⇑e ⇑e = 1

source

@[simp]

theorem Matrix.submatrix_one_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [One α] [DecidableEq m] [DecidableEq l] (e : l ≃ m) :

Matrix.submatrix 1 ⇑e ⇑e = 1

HepLean Documentation

Mathlib.Data.Matrix.Diagonal

Diagonal matrices #

Main definitions #