instModule — Mathlib

English

If 𝕜 is a semiring and γ a module over 𝕜 with suitable scalar action, then AEEqFun α γ μ forms a module over 𝕜.

Русский

Если 𝕜 — полупрямое кольцо и γ — модуль над 𝕜, то AEEqFun α γ μ образует модуль над 𝕜.

LaTeX

$$instModule : Module 𝕜 (α →ₘ[μ] γ)$$

Lean4

instance instModule [Semiring 𝕜] [AddCommMonoid γ] [ContinuousAdd γ] [Module 𝕜 γ] [ContinuousConstSMul 𝕜 γ] :
    Module 𝕜 (α →ₘ[μ] γ) :=
  toGerm_injective.module 𝕜 (toGermAddMonoidHom : (α →ₘ[μ] γ) →+ _) smul_toGerm

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