English
If M′-action on X is faithful and f: X → Y is an X-equivariant map that is injective, then the induced M′-action on Y is also faithful.
Русский
Если действие M′ на X аккуратно (безошибочно) отображает элементы M′ различно и отображение f: X→Y сохраняет X-действие и инъективно, то действие M′ на Y тоже оказывается верным (сдерживает инъективность).
LaTeX
$$$\text{If }\operatorname{FaithfulSMul}(M',X)\text{ and } f:X\to Y\text{ is }M'$-equivariant with $f$ injective,\; \operatorname{FaithfulSMul}(M',Y).$$$
Lean4
theorem _root_.FaithfulSMul.of_injective [FaithfulSMul M' X] [MulActionHomClass F M' X Y] (f : F)
(hf : Function.Injective f) : FaithfulSMul M' Y where
eq_of_smul_eq_smul {_ _} h := eq_of_smul_eq_smul fun m ↦ hf <| by simp_rw [map_smul, h]
