instMulDistribMulActionForallOfMulAction

English

There is a MulAction of DomMulAct M on MonoidHom A B, defined pointwise by (c • f) = f ∘ (MulDistribMulAction.toMonoidHom _ (mk.symm c)).

Русский

Существует действие MulAction DomMulAct M на моноидоморфизмах A → B, задаваемое точечно: (c • f) = f ∘ (toMonoidHom (mk.symm c)).

LaTeX

$$$\text{MulAction } (DomMulAct M) (MonoidHom A B)$ with $(c \cdot f)(a) = f(mk.symm c \cdot a)$$$

Lean4

instance {A : Type*} [Monoid M] [MulAction M α] [Monoid A] : MulDistribMulAction Mᵈᵐᵃ (α → A)
    where
  smul_mul _ _ _ := rfl
  smul_one _ := rfl

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