instMulSemiringActionSubtypeMem — Mathlib

English

If there is a faithful action of R' on α, then for any subsemiring S ≤ R' the induced action of S on α is faithful.

Русский

Если существует достоверное (верное) действие R' на α, то ограниченное действие S на α также является верным.

LaTeX

$$$FaithfulSMul S \ α$$$

Lean4

/-- The action by a subsemiring is the action by the underlying semiring. -/
instance [Semiring α] [MulSemiringAction R' α] (S : Subsemiring R') : MulSemiringAction S α :=
  inferInstance

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