distribSMul — Mathlib

English

The scalar action distributes over addition on the product: a · (x + y) = a · x + a · y, coordinatewise.

Русский

Смулл действует распределительно по сложению на произведении: a · (x + y) = a · x + a · y, по координатам.

LaTeX

$$$a \\cdot ((x_1, y_1) + (x_2, y_2)) = a \\cdot (x_1, y_1) + a \\cdot (x_2, y_2)$$$

Lean4

instance distribSMul {R M N : Type*} [AddZeroClass M] [AddZeroClass N] [DistribSMul R M] [DistribSMul R N] :
    DistribSMul R (M × N) where smul_add _ _ _ := by ext <;> exact smul_add ..

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