hadamard_one

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

M ⊙ 1 = diagonal of M's diagonal.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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