English
If f: B →* A is injective and smul is compatible with f via f(c • x) = c • f x, then B carries a MulDistribMulAction structure pulled back from A along f.
Русский
Если f: B →* A инъекция и действие совместимо с f через f(c • x) = c • f x, то B получает структуру MulDistribMulAction, перенесённую вдоль f.
LaTeX
$$$ f: B \to* A \text{ injective} \wedge (\forall c \in M, x \in B),\ f(c \cdot x) = c \cdot f(x) \;\Rightarrow\; \text{MulDistribMulAction } M B. $$$
Lean4
/-- Pushforward a multiplicative distributive multiplicative action along a surjective monoid
homomorphism. -/
-- See note [reducible non-instances]
protected abbrev mulDistribMulAction [Monoid B] [SMul M B] (f : A →* B) (hf : Surjective f)
(smul : ∀ (c : M) (x), f (c • x) = c • f x) : MulDistribMulAction M B
where
__ := hf.mulAction f smul
smul_mul c := by simp only [hf.forall, smul_mul', ← smul, ← f.map_mul, implies_true]
smul_one c := by rw [← f.map_one, ← smul, smul_one]
