left

Mathlib.Algebra.Group.Action.Defs

URI: https://scilib.ai/kg/mathlib#IsScalarTower.left

English

The left scalar-tower axiom holds: for all x,y,z, (xy) • z = x • (y • z).

Русский

Левый торовий скалярного действия выполняется: (xy) • z = x • (y • z).

LaTeX

$$$\\\\forall x,y \\\\in M, \\\\forall z \\\\in α, \\\\ (x\\\\cdot y) \\\\cdot z = x \\\\cdot (y \\\\cdot z).$$$

Lean4

@[to_additive]
instance left : IsScalarTower M M α where smul_assoc x y z := mul_smul x y z

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

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

Разделы

Аффилиация

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