diagonal_natCast'

Mathlib.Data.Matrix.Diagonal

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

English

Same as above, in a variant form: diagonal of m cast equals m cast.

Русский

То же самое в варианте: диагональ m.cast равна m.cast.

LaTeX

$$$\mathrm{diagonal}(\mathrm{cast}(m)) = \mathrm{cast}(m)$$$

Lean4

@[norm_cast]
theorem diagonal_natCast' [Zero α] [NatCast α] (m : ℕ) : diagonal ((m : n → α)) = m :=
  rfl

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

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

Разделы

Аффилиация

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