instModule — Mathlib

English

The space α →ᵇ β forms a 𝕜–module, with scalar multiplication defined pointwise and preserving addition.

Русский

Пространство α →ᵇ β образует 𝕜-модуль: скалярное умножение задается по точкам и сохраняет сложение.

LaTeX

$$$Module_{\\mathbb{K}}(\\alpha \\to^{\\mathrm{b}} \\beta)$$$

Lean4

instance instModule : Module 𝕜 (α →ᵇ β) :=
  DFunLike.coe_injective.module _ ⟨⟨_, coe_zero⟩, coe_add⟩ coe_smul

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