instMulActionForall — Mathlib

English

The DomMulAct construction lifts a MulAction to the function space α → β, defined pointwise: (c • f) (a) = f (mk.symm c • a).

Русский

Конструкция DomMulAct поднимает MulAction на пространство функций α → β по точечной формуле: (c • f)(a) = f(mk.symm c • a).

LaTeX

$$$\forall c \in DomMulAct M, \forall f : α \to β, \forall a : α: (c \cdot f)(a) = f(mk.symm c \cdot a)$$$

Lean4

@[to_additive]
instance [Monoid M] [MulAction M α] : MulAction Mᵈᵐᵃ (α → β)
    where
  one_smul f := funext fun _ ↦ congr_arg f (one_smul _ _)
  mul_smul _ _ f := funext fun _ ↦ congr_arg f (mul_smul _ _ _)

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