English
If a ∈ A i and b ∈ B j in a graded SMul context, then a • b is homogeneous of degree i +ᵥ j in B.
Русский
Если a ∈ A i и b ∈ B j в контексте градуированного SMul, то a • b однороден степени i +ᵥ j в B.
LaTeX
$$$ a ∈ A(i) \wedge b ∈ B(j) \Rightarrow a \cdot b ∈ B(i \,+\; j) $$$
Lean4
theorem graded_smul [VAdd ιA ιB] [SMul R M] {A : ιA → S} {B : ιB → N} [SetLike.GradedSMul A B] {a : R} {b : M} :
SetLike.IsHomogeneousElem A a → SetLike.IsHomogeneousElem B b → SetLike.IsHomogeneousElem B (a • b)
| ⟨i, hi⟩, ⟨j, hj⟩ => ⟨i +ᵥ j, SetLike.GradedSMul.smul_mem hi hj⟩