compHom — Mathlib

English

From a DistribMulAction on A, obtain a monoid hom from M to AddMonoid.End(A) by m ↦ (x ↦ m • x).

Русский

Из распределенного действия на A получить моноидный гомоморфизм из M в End(A), отображая m ↦ (x ↦ m•x).

LaTeX

$$$M \to^* \mathrm{AddMonoidEnd}(A)$ defined by $m \mapsto (x \mapsto m\cdot x)$$$

Lean4

/-- Compose a `MulDistribMulAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances]. -/
abbrev compHom [Monoid N] (f : N →* M) : MulDistribMulAction N A :=
  { MulAction.compHom A f with smul_one := fun x => smul_one (f x), smul_mul := fun x => smul_mul' (f x) }

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