English
Push forward a distributive multiplicative action along a surjective additive monoid homomorphism f: A →+ B, provided a compatibility Smul relation, to obtain a DistribMulAction M B.
Русский
Переносим распределенное умножающее действие вдоль сюръективного гомоморфа аддитивных моноидов f: A →+ B, при условии совместимости действия, получая DistribMulAction M B.
LaTeX
$$$(\text{Surjective}(f)) \land (\forall c\in M, x\in A,\ f(c\cdot x) = c\cdot f(x)) \Rightarrow \text{DistribMulAction}(M,B)$$$
Lean4
/-- Pushforward a distributive multiplicative action along a surjective additive monoid
homomorphism.
See note [reducible non-instances]. -/
protected abbrev distribMulAction [AddMonoid B] [SMul M B] (f : A →+ B) (hf : Surjective f)
(smul : ∀ (c : M) (x), f (c • x) = c • f x) : DistribMulAction M B :=
{ hf.distribSMul f smul, hf.mulAction f smul with }
