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

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

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

@[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

@[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

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

@[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

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

@[simp]

theorem Matrix.diagonal_zero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] : (diagonal fun (x : n) => 0) = 0

@[simp]

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

@[simp]

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

@[simp]

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

@[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

@[simp]

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

@[simp]

theorem Matrix.diagonal_neg {n : Type u_3} {α : Type v} [DecidableEq n] [NegZeroClass α] (d : n → α) : -diagonal d = diagonal fun (i : n) => -d i

@[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

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

@[implicit_reducible]

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

theorem Matrix.diagonal_natCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] (m : ℕ) : (diagonal fun (x : n) => ↑m) = ↑m

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

@[simp]

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

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

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

@[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

@[implicit_reducible]

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

theorem Matrix.diagonal_intCast {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] (m : ℤ) : (diagonal fun (x : n) => ↑m) = ↑m

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

@[simp]

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

@[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)

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

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)

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)

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)

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

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)

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

@[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)

@[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)

@[implicit_reducible]

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

@[simp]

theorem Matrix.diagonal_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] : (diagonal fun (x : n) => 1) = 1

@[simp]

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

@[simp]

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

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

@[simp]

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

@[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

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

@[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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

The diagonal of a square matrix.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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

@[simp]

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

theorem Matrix.diag_map {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : Matrix n n α} : (A.map f).diag = f ∘ A.diag

@[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

@[simp]

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

@[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

@[simp]

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

@[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

@[simp]

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

@[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

@[simp]

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

@[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

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.

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

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.

@[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)

@[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)

@[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

@[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