English
The family ⨂^i M carries the structure of a graded monoid with multiplication gMul, unit gOne, satisfying standard laws; i.e., the graded multiplication, unit, and associativity hold in each degree and are compatible across degrees.
Русский
Семейство ⨂^i M образует градуированный моноид с умножением gMul, единицей gOne и соответствующими законами совместимости между степенями.
LaTeX
$$instance gmonoid : GradedMonoid.GMonoid fun i => ⨂^R i M$$
Lean4
instance gmonoid : GradedMonoid.GMonoid fun i => ⨂[R]^i M :=
{ TensorPower.gMul,
TensorPower.gOne with
one_mul := fun _ => gradedMonoid_eq_of_cast (zero_add _) (one_mul _)
mul_one := fun _ => gradedMonoid_eq_of_cast (add_zero _) (mul_one _)
mul_assoc := fun _ _ _ => gradedMonoid_eq_of_cast (add_assoc _ _ _) (mul_assoc _ _ _) }
