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