English
The tensor product M ⊗_R N carries an additive commutative semigroup structure, inherited from the quotient construction, with addition compatible with the bilinear relations.
Русский
У тензорного произведения M ⊗_R N имеется структура AddCommSemigroup, полученная как фактор-общееобразование над bilinear relations.
LaTeX
$$$ (M \\otimes_R N) \\text{ is an AddCommSemigroup with operation induced by bilinearity relations.} $$$
Lean4
instance addZeroClass : AddZeroClass (M ⊗[R] N) :=
{ (addConGen (TensorProduct.Eqv R M N)).addMonoid with
/- The `toAdd` field is given explicitly as `TensorProduct.add` for performance reasons.
This avoids any need to unfold `Con.addMonoid` when the type checker is checking
that instance diagrams commute -/
toAdd := TensorProduct.add _ _
toZero := TensorProduct.zero _ _ }
