isLinearMap_smul' — Mathlib

English

For a fixed a ∈ M, the map c ↦ c · a from R to M is linear.

Русский

Для фиксированного вектора a ∈ M отображение c ↦ c · a по c из R в M является линейным.

LaTeX

$$$g(c) = c\cdot a$ defines a linear map $g: R \to M$; i.e., $g(c_1+c_2)=g(c_1)+g(c_2)$ and $g(r c)=r g(c)$.$$

Lean4

theorem isLinearMap_smul' {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) :
    IsLinearMap R fun c : R ↦ c • a :=
  IsLinearMap.mk (fun x y ↦ add_smul x y a) fun x y ↦ mul_smul x y a

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