lTensorOne'_tmul — Mathlib

English

For every y in R and n in N, the lTensorOne' map sends algebraMap_R_S(y) ⊗ n to y · n.

Русский

Для любого y ∈ R и n ∈ N отображение lTensorOne' отправляет algebraMap_R_S(y) ⊗ n в y · n.

LaTeX

$$$lTensorOne'(\mathsf{algebraMap}_R S(y) \otimes n) = y \cdot n.$$$

Lean4

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

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