diagonal_ofNat — Mathlib

English

For Zero α and NatCast α, and m ∈ ℕ, the diagonal matrix with entries ofNat(m) equals the OfNat.ofNat m matrix.

Русский

При нуле в α и NatCast α, для m ∈ ℕ диагональная матрица с элементами ofNat(m) равна матрице OfNat.ofNat m.

LaTeX

$$$\mathrm{diagonal}(\lambda _ : n . \mathrm{ofNat}(m)) = \mathrm{OfNat}.\mathrm{ofNat}(m)$$$

Lean4

theorem diagonal_ofNat [Zero α] [NatCast α] (m : ℕ) [m.AtLeastTwo] :
    diagonal (fun _ : n => (ofNat(m) : α)) = OfNat.ofNat m :=
  rfl

Похожие утверждения