diagonal_ofNat'

Mathlib.Data.Matrix.Diagonal

URI: https://scilib.ai/kg/mathlib#Matrix.diagonal_ofNat'

English

Variant: diagonal of m written via OfNat equals the corresponding OfNat value.

Русский

Вариант: диагональ m, записанная через OfNat, равна соответствующему значению OfNat.

LaTeX

$$$\mathrm{diagonal}(\mathrm{ofNat}(m)) = \mathrm{OfNat}.\mathrm{ofNat}(m)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru