instDistribSMulAEEqFun — Mathlib

English

Under AddMonoid and ContinuousAdd on β, AEEqFun α β μ carries a distributive scalar action of DomMulAct M.

Русский

При наличии AddMonoid и ContinuousAdd на β AEEqFun α β μ обладает распределённым скаляровым действием DomMulAct.

LaTeX

$$DistribSMul (DomMulAct M) (AEEqFun α β μ)$$

Lean4

instance [AddMonoid β] [ContinuousAdd β] : DistribSMul Mᵈᵐᵃ (α →ₘ[μ] β) where smul_add := by rintro _ ⟨⟩ ⟨⟩; rfl

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