smul_hadamard

Mathlib.LinearAlgebra.Matrix.Hadamard

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

English

For any scalar k and matrices A,B, (k • A) ⊙ B = k • (A ⊙ B).

Русский

Для любого скаляра k и матриц A,B выполняется (k • A) ⊙ B = k • (A ⊙ B).

LaTeX

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

Lean4

@[simp]
theorem smul_hadamard [Mul α] [SMul R α] [IsScalarTower R α α] (k : R) : (k • A) ⊙ B = k • A ⊙ B :=
  ext fun _ _ => smul_mul_assoc _ _ _

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

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

Разделы

Аффилиация

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