hadamard_smul

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

A ⊙ (k • B) = k • (A ⊙ B).

Русский

A ⊙ (k • B) = k • (A ⊙ B).

LaTeX

$$$A \odot (k \cdot B) = k \cdot (A \odot B)$$$

Lean4

@[simp]
theorem hadamard_smul [Mul α] [SMul R α] [SMulCommClass R α α] (k : R) : A ⊙ (k • B) = k • A ⊙ B :=
  ext fun _ _ => mul_smul_comm _ _ _

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

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

Разделы

Аффилиация

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