English
The inverse of quotientTensorQuotientEquiv, applied to Submodule.Quotient.mk (x ⊗ y), returns Submodule.Quotient.mk x ⊗ Submodule.Quotient.mk y.
Русский
Обратное quotientTensorQuotientEquiv применённое к Quot.mk (x ⊗ y) возвращает Quot.mk x ⊗ Quot.mk y.
LaTeX
$$$(\\text{quotientTensorQuotientEquiv}(m,n))^{-1}(\\mathrm{Submodule.Quotient.mk}(x \\otimes_R y)) = \\mathrm{Submodule.Quotient.mk} x \\otimes_R \\mathrm{Submodule.Quotient.mk} y$$$
Lean4
@[simp]
theorem rTensorOne_tmul (y : R) (m : M) : M.rTensorOne (m ⊗ₜ[R] algebraMap R _ y) = y • m :=
M.rTensorOne'_tmul y m