rTensorOne_tmul_one — Mathlib

English

Same as above: the inverse of quotientTensorQuotientEquiv sends Quot.mk (x ⊗ y) to Quot.mk x ⊗ Quot.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_one (m : M) : M.rTensorOne (m ⊗ₜ[R] 1) = m :=
  M.rTensorOne'_tmul_one m

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