English
Push forward the action of R on M along a compatible surjective map f : R →* S to obtain a DistribMulAction Left on M by S.
Русский
Перемещаем действие R на M вдоль совместной сюръективной карты f: R →* S, получая DistribMulAction на M над S.
LaTeX
$$$\text{Surjective } f \Rightarrow \text{DistribMulActionLeft}(R,S,M)$ with compatibility $f c \cdot x = c \cdot x$$$
Lean4
/-- Push forward the action of `R` on `M` along a compatible surjective map `f : R →* S`.
See also `Function.Surjective.mulActionLeft` and `Function.Surjective.moduleLeft`.
-/
abbrev distribMulActionLeft {R S M : Type*} [Monoid R] [AddMonoid M] [DistribMulAction R M] [Monoid S] [SMul S M]
(f : R →* S) (hf : Function.Surjective f) (hsmul : ∀ (c) (x : M), f c • x = c • x) : DistribMulAction S M :=
{ hf.distribSMulLeft f hsmul, hf.mulActionLeft f hsmul with }
