isLinearMap_smul — Mathlib

English

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

Русский

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

LaTeX

$$$f(z) = c\cdot z$ defines a linear map $f: M \to M$; i.e., $f(x+y)=f(x)+f(y)$ and $f(rz)=r f(z)$ for all x,y, r.$$

Lean4

theorem isLinearMap_smul {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :
    IsLinearMap R fun z : M ↦ c • z := by
  refine IsLinearMap.mk (smul_add c) ?_
  intro _ _
  simp only [smul_smul, mul_comm]

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