toNatLinearMap — Mathlib

English

Given an additive group homomorphism f: M →+ M₂, one obtains a natural-number-linear map f^ℕ: M →ₗ[ℕ] M₂ with same action on elements.

Русский

Дано композиционное дополнение f: M →+ M₂, получаем ℕ-линейное отображение f^ℕ: M →ₗ[ℕ] M₂ с тем же действием на элементы.

LaTeX

$$$f: M \to_+ M_2 \;\Rightarrow\; f \mapsto f^{\mathbb{N}}: M \to_\ℕ M_2$, с $(f^{\mathbb{N}})(x)=f(x)$.$$

Lean4

/-- Reinterpret an additive homomorphism as an `ℕ`-linear map. -/
def toNatLinearMap [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) : M →ₗ[ℕ] M₂
    where
  toFun := f
  map_add' := f.map_add
  map_smul' := map_nsmul f

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