tensorObj — Mathlib

English

Auxiliary construction giving the tensor product object of two quadratic modules, with form given by the tmul of the forms.

Русский

Вспомогательное построение тензорного произведения двух квадратичных модулей с формой, равной tmul форм.

LaTeX

$$$ \\text{tensorObj}(X,Y) = \\text{of}(X.form \\; \\text{tmul} \\; Y.form). $$$

Lean4

/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`. -/
@[simps! form]
abbrev tensorObj (X Y : QuadraticModuleCat.{u} R) : QuadraticModuleCat.{u} R :=
  of (X.form.tmul Y.form)

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