right

Mathlib.Algebra.Algebra.Defs

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

English

The scalar action of R on A is compatible with multiplication on A: (r • x) · y = r • (x · y) for r ∈ R and x,y ∈ A.

Русский

Скалярное действие R на A совместимо с умножением: (r • x) · y = r • (x · y).

LaTeX

$$$r \cdot x \cdot y = r \cdot (x \cdot y)$$$

Lean4

instance _root_.IsScalarTower.right : IsScalarTower R A A :=
  ⟨fun x y z => by rw [smul_eq_mul, smul_eq_mul, smul_def, smul_def, mul_assoc]⟩

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

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

Разделы

Аффилиация

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