English
An internal graded SMul structure on A is obtained from the graded multiplication: for homogeneous a ∈ A i and b ∈ A j, the product a*b lies in A(i+j) and provides the SMul action.
Русский
Внутренняя градуированная структура умножения на A порождается градуированным умножением: для однородных a ∈ A i и b ∈ A j произведение a*b лежит в A(i+j) и задаёт действие SMul.
LaTeX
$$$ \forall i,j,\ a ∈ A(i), b ∈ A(j) \Rightarrow a b ∈ A(i+j) $$$
Lean4
/-- Internally graded version of `Mul.toSMul`. -/
instance toGradedSMul [AddMonoid ιA] [Monoid R] {S : Type*} [SetLike S R] (A : ιA → S) [SetLike.GradedMonoid A] :
SetLike.GradedSMul A A where smul_mem _ _ _ _ hi hj := SetLike.GradedMonoid.toGradedMul.mul_mem hi hj
