instSMul

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.instSMul

English

There is a scalar action on the product: a • (x, y) = (a • x, a • y).

Русский

Скалярное действие на произведении: a • (x, y) = (a • x, a • y).

LaTeX

$$a \cdot (x,y) = (a \cdot x, a \cdot y)$$

Lean4

@[to_additive]
instance instSMul : SMul M (α × β) where smul a p := (a • p.1, a • p.2)

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

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

Разделы

Аффилиация

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