compHom — Mathlib

English

Compose a DistribMulAction with a MonoidHom f : M →* N to obtain a DistribMulAction N on A, i.e. an action via f.

Русский

Скомпонуем DistribMulAction с MonoidHom f : M →* N, получив DistribMulAction N на A, то есть действие через f.

LaTeX

$$$\text{DistribMulAction}(M,A) \Rightarrow \text{DistribMulAction}(N,A)$ via $f: N \leftarrow M$$$

Lean4

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

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