faithfulSMul — Mathlib

English

The natural R-action on the AddMonoidAlgebra k[G] is faithful provided k is a semiring, R acts faithfully on k, and G is nonempty.

Русский

Естественное действие R на AddMonoidAlgebra k[G] является верным (faithful) при условии, что k — полугруппа, R действует верно на k, и G непуст.

LaTeX

$$$$\text{FaithfulSMul } R k[G].$$$$

Lean4

instance faithfulSMul [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R k[G] :=
  Finsupp.faithfulSMul

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