sum_hadamard_eq

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

For A,B with compatible sizes, the sum over all entries of A ⊙ B equals the trace of A B^T.

Русский

Для матриц A,B подходящих размеров сумма по всем элементам произведения A ⊙ B равна следу матрицы A B^T.

LaTeX

$$$\sum_{i}\sum_{j} (A \odot B)_{ij} = \operatorname{trace}(A B^T)$$$

Lean4

theorem sum_hadamard_eq : (∑ i : m, ∑ j : n, (A ⊙ B) i j) = trace (A * Bᵀ) :=
  rfl

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

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

Разделы

Аффилиация

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