smul_tmul — Mathlib

English

The tensor product carries an additive commutative semigroup structure, where addition is induced from the quotient construction.

Русский

Тензорное произведение имеет структуру AddCommSemigroup, где сложение задаётся через отношение эквивалентности фактора.

LaTeX

$$$ (M \\otimes_R N) \\text{ is an AddCommSemigroup}. $$$

Lean4

/-- `smul` can be moved from one side of the product to the other . -/
theorem smul_tmul [DistribMulAction R' N] [CompatibleSMul R R' M N] (r : R') (m : M) (n : N) :
    (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n) :=
  CompatibleSMul.smul_tmul _ _ _

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