instFaithfulSMulSubtypeMem — Mathlib

English

If a ring R acts faithfully on α, then the restricted action of any subring S ≤ R on α is also faithful.

Русский

Если R действует верно на α с существенной связью, то ограниченное до подкольца S ≤ R действие на α также будет верным.

LaTeX

$$$\text{FaithfulSMul}\; S\; \alpha$$$

Lean4

instance [SMul R α] [FaithfulSMul R α] (S : Subring R) : FaithfulSMul S α :=
  inferInstanceAs (FaithfulSMul S.toSubsemiring α)

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