addMonoid — Mathlib

English

The tensor product M ⊗_R N carries a natural additive monoid structure, compatible with the tensor product operations.

Русский

Тензорное произведение M ⊗_R N имеет естественную структуру аддитивного моноида, совместимую с тензорной операцией.

LaTeX

$$$\text{AddMonoid}(M \otimes_R N)$$$

Lean4

instance addMonoid : AddMonoid (M ⊗[R] N) :=
  {
    TensorProduct.addZeroClass _ _ with
    toAddSemigroup := TensorProduct.addSemigroup _ _
    toZero := TensorProduct.zero _ _
    nsmul := fun n v => n • v
    nsmul_zero := by simp [TensorProduct.zero_smul]
    nsmul_succ := by simp only [TensorProduct.one_smul, TensorProduct.add_smul, add_comm, forall_const] }

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