English
If f: α → β is injective and respects the actions (h₁, h₂), then SMulCommClass M N α follows from SMulCommClass M N β via f.
Русский
Если f: α → β инъективно и сохраняет действия (h₁, h₂), то из SMulCommClass M N β следует SMulCommClass M N α.
LaTeX
$$$ f \text{ injective} \wedge (\forall c,x, f(c \cdot x) = c \cdot f(x)) \wedge (\forall c,x, f(c \cdot x) = c \cdot f(x)) \Rightarrow SMulCommClass M N α. $$$
Lean4
@[to_additive]
theorem smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β] [SMulCommClass M N β] {f : α → β} (hf : Injective f)
(h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) : SMulCommClass M N α where
smul_comm c₁ c₂ x := hf <| by simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]
