quotTensorEquivQuotSMul_mk_tmul — Mathlib

English

The quotient-tensor-smul map evaluated at a pure tensor equals the class of the scaled module element.

Русский

Отображение через факторизацию-умножение равно классу масштабирующего элемента модуля.

LaTeX

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

Lean4

@[simp]
theorem quotTensorEquivQuotSMul_mk_tmul (I : Ideal R) (r : R) (x : M) :
    quotTensorEquivQuotSMul M I (Ideal.Quotient.mk I r ⊗ₜ[R] x) = Submodule.Quotient.mk (r • x) :=
  (quotTensorEquivQuotSMul M I).eq_symm_apply.mp <|
    Eq.trans
        (congrArg (· ⊗ₜ[R] x) <|
          Eq.trans (congrArg (Ideal.Quotient.mk I) (Eq.trans (smul_eq_mul ..) (mul_one r))).symm <|
            Submodule.Quotient.mk_smul I r 1) <|
      smul_tmul r _ x

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