diagonal_intCast

Mathlib.Data.Matrix.Diagonal

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

English

If α has 0 and an IntCast, then the diagonal of m (as α) equals m.cast.

Русский

Если в α есть 0 и IntCast, диагональная матрица с m как элемент α равна m.cast.

LaTeX

$$$\mathrm{diagonal}(\lambda _ . (m : \alpha)) = m$$$

Lean4

@[norm_cast]
theorem diagonal_intCast [Zero α] [IntCast α] (m : ℤ) : diagonal (fun _ : n => (m : α)) = m :=
  rfl

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

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

Разделы

Аффилиация

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