English
If α is nonempty, M has a Zero and a faithful SMul, then the induced action on Finsupp α M is faithful: scalars are determined by their action on basis elements single a m.
Русский
Если множество индексов непусто и существна нулевая структура, то действие на Finsupp α M тоже является верным; нуль-скаляр не порождает неточности.
LaTeX
$$$\\text{FaithfulSMul } R (\\alpha \\to_0 M)$, при условии\\n[Nonempty α] [Zero M] [SMulZeroClass R M] [FaithfulSMul R M]$$
Lean4
instance faithfulSMul [Nonempty α] [Zero M] [SMulZeroClass R M] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M) where
eq_of_smul_eq_smul
h :=
let ⟨a⟩ := ‹Nonempty α›
eq_of_smul_eq_smul fun m : M => by simpa using DFunLike.congr_fun (h (single a m)) a
