isScalarTower_right — Mathlib

English

The scalar action of a ring R on the graded monoid A is compatible with the graded multiplication; i.e., (r • a) • b = r • (a • b).

Русский

Действие скаляра из кольца R на градуированную моноиду A совместимо с градуированным умножением: (r • a) • b = r • (a • b).

LaTeX

$$$\\forall r\\in R, a,b\\in A:\\; (r\\cdot a)\\cdot b = r\\cdot (a\\cdot b).$$$

Lean4

instance _root_.GradedMonoid.isScalarTower_right : IsScalarTower R (GradedMonoid A) (GradedMonoid A) where
  smul_assoc s x
    y := by
    dsimp
    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc]

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