Documentation

Mathlib.Data.Matrix.Diagonal

Diagonal matrices #

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

Main definitions #

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
    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_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_7} {α : 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
      instance Matrix.instNatCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [NatCast α] :
      NatCast (Matrix n n α)
      Equations
        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
        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
        instance Matrix.instIntCastOfZero {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [IntCast α] :
        IntCast (Matrix n n α)
        Equations
          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_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.diagonal_unique {m : Type u_2} {α : Type v} [Unique m] [DecidableEq m] [Zero α] (d : m → α) :
          diagonal d = of fun (x x : 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 Matrix.one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :
          One (Matrix n n α)
          Equations
            source
            @[simp]
            theorem Matrix.diagonal_one {n : Type u_3} {α : Type v} [DecidableEq n] [Zero α] [One α] :
            (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) :
            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
              source
              instance Matrix.instAddGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddGroupWithOne α] :
              AddGroupWithOne (Matrix n n α)
              Equations
                source
                instance Matrix.instAddCommMonoidWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommMonoidWithOne α] :
                AddCommMonoidWithOne (Matrix n n α)
                Equations
                  source
                  instance Matrix.instAddCommGroupWithOne {n : Type u_3} {α : Type v} [DecidableEq n] [AddCommGroupWithOne α] :
                  AddCommGroupWithOne (Matrix n n α)
                  Equations
                    source
                    def Matrix.diag {n : Type u_3} {α : Type v} (A : Matrix n n α) (i : n) :
                    α

                    The diagonal of a square matrix.

                    Equations
                      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_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 α] :
                        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.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_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