hadamard_add

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

Hadamard product distributes over addition in the second argument: A ⊙ (B + C) = A ⊙ B + A ⊙ C.

Русский

Hadamard-произведение распределяется по сложению по второму аргументу: A ⊙ (B + C) = A ⊙ B + A ⊙ C.

LaTeX

$$$A \odot (B + C) = A \odot B + A \odot C$$$

Lean4

theorem hadamard_add [Distrib α] : A ⊙ (B + C) = A ⊙ B + A ⊙ C :=
  ext fun _ _ => left_distrib _ _ _

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

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

Разделы

Аффилиация

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