smulCommClass_right — Mathlib

English

The graded monoid with coefficients has a scalar action from a base ring that commutes with the multiplication on the right: for all r, a, b, r • (a ⋅ b) = (r • a) ⋅ b = a ⋅ (r • b).

Русский

Градуированная моноида с коэффициентами имеет действие скаляров из базового кольца, которое справа commuting с умножением: для всех r, a, b выполняется r • (a · b) = (r • a) · b = a · (r • b).

LaTeX

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

Lean4

instance _root_.GradedMonoid.smulCommClass_right : SMulCommClass R (GradedMonoid A) (GradedMonoid A) where
  smul_comm s x
    y := by
    dsimp
    rw [GAlgebra.smul_def, GAlgebra.smul_def, ← mul_assoc, GAlgebra.commutes, mul_assoc]

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