instIsScalarTowerRight — Mathlib

English

For any DivisionRing R, the rationals ℚ act on R in a scalar-tower manner: (a) · (x y) = (a · x) y for all a ∈ ℚ and x,y ∈ R.

Русский

Для любого делимого кольца R скаляры из ℚ действуют на R в виде цепочки: (a)·(x y) = (a·x) y для всех a ∈ ℚ и x,y ∈ R.

LaTeX

$$$\\forall a \\in \\mathbb{Q}, \\forall x,y \\in R:\\ a \\cdot (x y) = (a \\cdot x) y$$$

Lean4

instance instIsScalarTowerRight : IsScalarTower ℚ R R where
  smul_assoc a x y := by simp only [smul_def, smul_eq_mul, mul_assoc]

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