instFaithfulSMulSubtypeMem — Mathlib

English

For any subalgebra S, the induced FaithfulSMul instance on the subtype mem S x α holds; i.e., the action of S on α is faithful.

Русский

Для любой подалгебры S действует верное (Faithful)SMul на типе Subtype mem S x α: действие S на α верно детерминирует элементы.

LaTeX

$$$\text{FaithfulSMul}(\Subtype{ x \in S}, \alpha)$$$

Lean4

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

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