tensorQuotientEquiv_symm_apply_tmul_mk

English

The inverse isomorphism applied to the class of x ⊗ ȳ yields x ⊗ ȳ, where ȳ denotes the class of y in the quotient.

Русский

Обратное отображение применено к классу x ⊗ ȳ дает x ⊗ ȳ, где ȳ — класс y в фактор-модуле.

LaTeX

$$$$(\text{tensorQuotientEquiv } M\, n)^{-1}([x \otimes y]) = x \otimes [y],$$$$

Lean4

@[simp]
theorem tensorQuotientEquiv_symm_apply_tmul_mk (n : Submodule R N) (x : M) (y : N) :
    (tensorQuotientEquiv M n).symm (Submodule.Quotient.mk (x ⊗ₜ y)) = x ⊗ₜ[R] Submodule.Quotient.mk y :=
  rfl

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