compHom_smul_def — Mathlib

English

A monoid homomorphism can push forward a group action to a new action.

Русский

Гомоморфизм моноидов может переносить действие на новое действие.

LaTeX

$$$\\mathrm{MulAction}(N, α)$ with smul defined by $f$ as in the construction.$$

Lean4

@[to_additive]
theorem compHom_smul_def {E F G : Type*} [Monoid E] [Monoid F] [MulAction F G] (f : E →* F) (a : E) (x : G) :
    letI : MulAction E G := MulAction.compHom _ f
    a • x = (f a) • x :=
  rfl

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