English
For homogeneous elements x ∈ A i and y ∈ B j, the value of the graded SMul built from A and B coincides with the plain product of the underlying values: the smul in the ambient object is x.1 • y.1.
Русский
Для однородных элементов x ∈ A i и y ∈ B j значение градуированного умножения на основе A и B совпадает с обычным произведением их базовых значений: x.1 • y.1.
LaTeX
$$$ (@GradedMonoid.GSMul.smul\; i\; j\; x\; y) = x.1 \cdot y.1 $$$
Lean4
@[simp]
theorem coe_GSMul {S R N M : Type*} [SetLike S R] [SetLike N M] [SMul R M] [VAdd ιA ιB] (A : ιA → S) (B : ιB → N)
[SetLike.GradedSMul A B] {i : ιA} {j : ιB} (x : A i) (y : B j) :
(@GradedMonoid.GSMul.smul ιA ιB (fun i ↦ A i) (fun i ↦ B i) _ _ i j x y : M) = x.1 • y.1 :=
rfl
