tensorQuotEquivQuotSMul_tmul_mk — Mathlib

English

The isomorphism sends x ⊗ ȳ to ȳ ⊗ x in the appropriate swapped tensor context.

Русский

Изоморфизм отправляет x ⊗ ȳ в ȳ ⊗ x в соответствующем контексте перемещённого тензорного произведения.

LaTeX

$$$$ \text{tensorQuotEquivQuotSMul}_M I\big( x \otimes (\overline{y}) \big) = \overline{r x}. $$$$

Lean4

@[simp]
theorem tensorQuotEquivQuotSMul_tmul_mk (I : Ideal R) (x : M) (r : R) :
    tensorQuotEquivQuotSMul M I (x ⊗ₜ[R] Ideal.Quotient.mk I r) = Submodule.Quotient.mk (r • x) :=
  quotTensorEquivQuotSMul_mk_tmul I r x

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