smulRight — Mathlib

English

If f is an R-linear map from M₁ to S and x ∈ M, then the map b ↦ f(b) · x is an R-linear map from M₁ to M.

Русский

Если f: M₁ →ₗ[R] S и x ∈ M, то отображение b ↦ f(b) · x задаёт R-линейное отображение M₁ → M.

LaTeX

$$smulRight(f, x) : M₁ →ₗ[R] M так, что for all b ∈ M₁, (smulRight f x)(b) = f(b) · x.$$

Lean4

/-- When `f` is an `R`-linear map taking values in `S`, then `fun b ↦ f b • x` is an `R`-linear
map. -/
def smulRight (f : M₁ →ₗ[R] S) (x : M) : M₁ →ₗ[R] M
    where
  toFun b := f b • x
  map_add' x y := by rw [f.map_add, add_smul]
  map_smul' b y := by rw [RingHom.id_apply, map_smul, smul_assoc]

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