mul_smul_mul_eq_smul_mul_smul

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.mul_smul_mul_eq_smul_mul_smul

English

Distributes scalars across product: (x y) • (M N) = (x • M) * (y • N).

Русский

Распределение скаляров над произведением: (x y) • (M N) = (x • M) * (y • N).

LaTeX

$$$ (x \\cdot y) \\cdot (M \\cdot N) = (x \\cdot M) \\cdot (y \\cdot N) $$$

Lean4

theorem mul_smul_mul_eq_smul_mul_smul (x y : R) : (x * y) • (M * N) = (x • M) * (y • N) :=
  mul_smul_mul_comm x y M N

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

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

Разделы

Аффилиация

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