tensorQuotientEquiv_apply_mk_tmul

English

The isomorphism sends a pure tensored element x ⊗ ȳ to its canonical representative x ⊗ y modulo the submodule M ⊗ n.

Русский

Изоморфизм переводит элемент x ⊗ ȳ в канонический представитель x ⊗ y по модулю M ⊗ n.

LaTeX

$$$$ \text{tensorQuotientEquiv}_M^n\big(x \otimes (y + n)\big) = (x \otimes y) + (M \otimes n). $$$$

Lean4

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

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