diagonal_intCast'

Mathlib.Data.Matrix.Diagonal

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

English

Variant: diagonal of m (as integer cast) equals m cast.

Русский

Вариант: диагональ m.cast равна m.cast.

LaTeX

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

Lean4

@[norm_cast]
theorem diagonal_intCast' [Zero α] [IntCast α] (m : ℤ) : diagonal ((m : n → α)) = m :=
  rfl

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

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

Разделы

Аффилиация

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