English
There is a graded multiplication on tensor powers: for a ∈ ⨂^i M and b ∈ ⨂^j M, their product a ₜ* b lies in ⨂^{i+j} M and is defined using the mulEquiv map applied to the tensor a ⊗ b.
Русский
Существуют градуированное умножение на тензорные степени: для a ∈ ⨂^i M и b ∈ ⨂^j M их произведение a ₜ* b лежит в ⨂^{i+j} M и определяется через отображение mulEquiv на a ⊗ b.
LaTeX
$$$a \\ ₜ*\\ b := (TensorProduct.mk R _ _).compr₂ (↑(mulEquiv : _ ≃ₗ[R] (⨂^{i+j} M))) (a ⊗ b)$$$
Lean4
/-- As a graded monoid, `⨂[R]^i M` has a `(*) : ⨂[R]^i M → ⨂[R]^j M → ⨂[R]^(i + j) M`. -/
instance gMul : GradedMonoid.GMul fun i => ⨂[R]^i M where
mul {i j} a b := (TensorProduct.mk R _ _).compr₂ (↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(i + j)) M)) a b
