one_hadamard

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

1 ⊙ M = diagonal of M's diagonal.

Русский

1 ⊙ M = диагональ матрицы M.

LaTeX

$$$1 \odot M = \operatorname{diagonal}(\lambda i. M_{ii})$$$

Lean4

theorem one_hadamard : (1 : Matrix n n α) ⊙ M = diagonal fun i => M i i :=
  by
  ext i j
  by_cases h : i = j <;> simp [h]

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

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

Разделы

Аффилиация

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