rTensorOne_tmul — Mathlib

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

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