rTensorOne'_tmul — Mathlib

English

For y ∈ R and m ∈ M, M.rTensorOne'(m ⊗ algebraMap y) = y m; in particular, combining with 1 gives the unit action.

Русский

Для y ∈ R и m ∈ M, M.rTensorOne'(m ⊗ algebraMap y) = y m; в частности, при y=1 получаем единичное действие.

LaTeX

$$$M.lTensorOne'(m \\otimes_R \\mathrm{algebraMap}_R^S(y)) = y \\cdot m$$$

Lean4

@[simp]
theorem rTensorOne'_tmul (y : R) (m : M) : M.rTensorOne' (m ⊗ₜ[R] algebraMap R _ y) = y • m :=
  Subtype.val_injective <|
    by
    simp_rw [rTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.coe_ofEq_apply,
      LinearMap.codRestrict_apply, SetLike.val_smul]
    rw [Algebra.smul_def, Algebra.commutes]
    exact mulMap_tmul M _ _ _

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