instAddCommMonoid — Mathlib

English

PiTensorProduct(R,s) carries an additive commutative monoid structure under the induced addition.

Русский

PiTensorProduct(R,s) имеет структуру аддитивного коммутативного моноида под индуцируемым сложением.

LaTeX

$$$\text{AddCommMonoid}(\PiTensorProduct(R,s))$$$

Lean4

instance : AddCommMonoid (⨂[R] i, s i) :=
  { (addConGen (PiTensorProduct.Eqv R s)).addMonoid with
    add_comm := fun x y ↦
      AddCon.induction_on₂ x y fun _ _ ↦ Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.add_comm _ _ }

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