English
The canonical quotient tensor-quotient equivalence maps (x ⊗ y) formed from representatives to the tensor product of the quotients: quotientTensorQuotientEquiv m n (Submodule.Quotient.mk x ⊗ Submodule.Quotient.mk y) = Submodule.Quotient.mk (x ⊗ y).
Русский
Каноническое эквивалентное отображение тензорного произведения частных подмодулей переводит произведение представителей в тензор произведение частот: quotientTensorQuotientEquiv m n (Submodule.Quotient.mk x ⊗ y) = Submodule.Quotient.mk (x ⊗ y).
LaTeX
$$$\\text{quotientTensorQuotientEquiv}(m,n)(\\mathrm{Submodule.Quotient.mk}\\,x \\otimes_R \\mathrm{Submodule.Quotient.mk}\\,y) = \\mathrm{Submodule.Quotient.mk}(x \\otimes y)$$$
Lean4
@[simp]
theorem quotientTensorQuotientEquiv_symm_apply_mk_tmul (m : Submodule R M) (n : Submodule R N) (x : M) (y : N) :
(quotientTensorQuotientEquiv m n).symm (Submodule.Quotient.mk (x ⊗ₜ y)) =
Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y :=
rfl
