instDistribMulAction — Mathlib

English

If 𝕜 is a semiring and γ a module with appropriate distributive actions, then AEEqFun α γ μ is a distributive-multiplicative action module over 𝕜.

Русский

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

LaTeX

$$instDistribMulAction : DistribMulAction 𝕜 (α →ₘ[μ] γ)$$

Lean4

instance instDistribMulAction [Monoid 𝕜] [AddMonoid γ] [ContinuousAdd γ] [DistribMulAction 𝕜 γ]
    [ContinuousConstSMul 𝕜 γ] : DistribMulAction 𝕜 (α →ₘ[μ] γ) :=
  toGerm_injective.distribMulAction (toGermAddMonoidHom : (α →ₘ[μ] γ) →+ _) fun c : 𝕜 => smul_toGerm c

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