quotTensorEquivQuotSMul_symm_mk — Mathlib

English

The symmetrized version of the quotient-tensor-smul sends x ⊗ ȳ to x ⊗ 1̄ in the appropriate quotient setting.

Русский

Симметрированная версия отображения квоты-тензорного умножения отправляет x ⊗ ȳ в x ⊗ 1̄ в нужном фактор-модуле.

LaTeX

$$$$ (\text{quotTensorEquivQuotSMul M I}).symm (\overline{x}) = x \otimes 1. $$$$

Lean4

@[simp]
theorem quotTensorEquivQuotSMul_symm_mk (I : Ideal R) (x : M) :
    (quotTensorEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = 1 ⊗ₜ[R] x :=
  rfl

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