English
The tensor product M ⊗_R N is defined as the quotient of the free additive monoid on M × N by the bilinear relations encoding linearity in each argument.
Русский
Тензорное произведение M ⊗_R N определяется как фактор-обобщение свободной аддитивной моноиды на M × N по реляциям билинейности по каждому аргументу.
LaTeX
$$$ M \\otimes_R N \\;=\\; (\\mathrm{FreeAddMonoid})(M \\times N) \\big/ \\sim, \\quad \\sim \\text{ generated by bilinearity relations}. $$$
Lean4
/-- The tensor product of two modules `M` and `N` over the same commutative semiring `R`.
The localized notations are `M ⊗ N` and `M ⊗[R] N`, accessed by `open scoped TensorProduct`. -/
def TensorProduct : Type _ :=
(addConGen (TensorProduct.Eqv R M N)).Quotient
