diagonal_natCast — Mathlib

English

For any natural m, the diagonal matrix with every diagonal entry equal to m (in α) is equal to the NatCast of m as a matrix.

Русский

Для любого натурального m диагональная матрица, у которой на диагонали стоит m, равна natCast(m) как матрица.

LaTeX

$$$\mathrm{diagonal}(\text{const}_n(m)) = m$$$

Lean4

@[norm_cast]
theorem diagonal_natCast [Zero α] [NatCast α] (m : ℕ) : diagonal (fun _ : n => (m : α)) = m :=
  rfl

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