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.

This is available in bundled forms as:

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) :

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) :

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) :

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) :

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

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

source

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

Function.Injective diagonal

source

@[simp]

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

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

source

@[simp]

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

diagonal 0 = 0

source

@[simp]

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

diagonal d = 0 ↔ d = 0

source

@[simp]

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

(diagonal v).transpose = diagonal v

source

@[simp]

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

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

source

@[simp]

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

diagonal (r • d) = r • diagonal d

source

@[simp]

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

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

source

@[simp]

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

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

source

theorem Matrix.diagonal_mem_matrix_iff {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] {S : Set α} (hS : 0 ∈ S) {d : n → α} :

diagonal d ∈ S.matrix ↔ ∀ (i : n), d i ∈ S

source

@[instance_reducible]

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 : ℕ) :

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

source

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

diagonal ↑m = ↑m

source

@[simp]

theorem Matrix.diagonal_eq_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] {d : n → α} {m : ℕ} :

diagonal d = ↑m ↔ d = ↑m

source

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

(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] :

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

source

@[simp]

theorem Matrix.diagonal_eq_ofNat {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] {d : n → α} {m : ℕ} [m.AtLeastTwo] :

diagonal d = OfNat.ofNat m ↔ d = OfNat.ofNat m

source

@[instance_reducible]

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 : ℤ) :

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

source

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

diagonal ↑m = ↑m

source

@[simp]

theorem Matrix.diagonal_eq_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] {d : n → α} {m : ℤ} :

diagonal d = ↑m ↔ d = ↑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 → α} :

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

source

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

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

source

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

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

source

theorem Matrix.natCast_apply {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {i j : n} {d : ℕ} :

↑d i j = ↑(if i = j then d else 0)

source

theorem Matrix.ofNat_apply {n : Type u_3} {α : Type v} [DecidableEq n] [AddMonoidWithOne α] {i j : n} {d : ℕ} [d.AtLeastTwo] :

(OfNat.ofNat d) i j = ↑(if i = j then d else 0)

source

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

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

source

theorem Matrix.intCast_apply {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] {i j : n} {d : ℤ} :

↑d i j = ↑(if i = j then d else 0)

source

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

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

source

@[simp]

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

(diagonal d).col i = Pi.single i (d i)

source

@[simp]

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

(diagonal d).row j = Pi.single j (d j)

source

@[instance_reducible]

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

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

source

@[simp]

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

diagonal 1 = 1

source

@[simp]

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

diagonal d = 1 ↔ d = 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) :

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_reducible]

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

AddMonoidWithOne (Matrix n n α)

Equations

Matrix.instAddMonoidWithOne = { toNatCast := Matrix.instNatCastOfZero, toAddMonoid := Matrix.addMonoid, toOne := Matrix.one, natCast_zero := ⋯, natCast_succ := ⋯ }

source

@[instance_reducible]

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

AddGroupWithOne (Matrix n n α)

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

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

AddCommMonoidWithOne (Matrix n n α)

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

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

AddCommGroupWithOne (Matrix n n α)

Equations

One or more equations did not get rendered due to their size.

source

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

The diagonal of a square matrix.

This is available in bundled forms as:

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 → α) :

(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 α] :

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_4} {α : 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 α] :

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 = diagonal v ↔ M = diagonal v

source

@[simp]

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

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) :

(diagonal d).submatrix e e = 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) :

submatrix 1 e e = 1

source

theorem Matrix.submatrix_ofNat {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [NatCast α] [DecidableEq m] [DecidableEq l] (e : l → m) (he : Function.Injective e) (k : ℕ) [k.AtLeastTwo] :

(OfNat.ofNat k).submatrix e e = OfNat.ofNat k

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) :

(diagonal d).submatrix ⇑e ⇑e = 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) :

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

source

@[simp]

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

A.submatrix ⇑e ⇑e = diagonal d ↔ A = diagonal (d ∘ ⇑e.symm)

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) :

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) :

submatrix 1 ⇑e ⇑e = 1

source

@[simp]

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

A.submatrix ⇑e ⇑e = 1 ↔ A = 1

source

@[simp]

theorem Matrix.submatrix_ofNat_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [NatCast α] [DecidableEq m] [DecidableEq l] (e : l ↪ m) (k : ℕ) [k.AtLeastTwo] :

(OfNat.ofNat k).submatrix ⇑e ⇑e = OfNat.ofNat k

source

@[simp]

theorem Matrix.submatrix_ofNat_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [NatCast α] [DecidableEq m] [DecidableEq l] (e : l ≃ m) (k : ℕ) [k.AtLeastTwo] :

(OfNat.ofNat k).submatrix ⇑e ⇑e = OfNat.ofNat k

source

@[simp]

theorem Matrix.submatrix_equiv_eq_ofNat_iff {l : Type u_1} {m : Type u_2} {α : Type v} [Zero α] [NatCast α] [DecidableEq m] [DecidableEq l] {A : Matrix m m α} {e : l ≃ m} (k : ℕ) [k.AtLeastTwo] :

A.submatrix ⇑e ⇑e = OfNat.ofNat k ↔ A = OfNat.ofNat k

Documentation

Mathlib.Data.Matrix.Diagonal

Diagonal matrices #

Main definitions #