graded_smul — Mathlib

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⟩

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