instFaithfulSMulOfNonempty — Mathlib

English

If α is nonempty and M is a faithful SMul module over R, then Finsupp α M carries a faithful R-action. In particular, the map r ↦ (f ↦ r • f) is injective.

Русский

Если α непусто и M — достоверная модульная подструктура над R, то Finsupp α M имеет достоверное действие над R. То есть отображение r ↦ (f ↦ r • f) инъективно.

LaTeX

$$$\\text{Nonempty}(α)\\land \\text{FaithfulSMul}(R,M)\\;\\Rightarrow\\; \\text{FaithfulSMul}(R, α \\to_0 M)$$$

Lean4

instance [Nonempty α] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M) :=
  .of_injective (Finsupp.lsingle <| Classical.arbitrary _) (Finsupp.single_injective _)

Похожие утверждения