faithfulSMul — Mathlib

English

If a submonoid S of M' acts on α via a faithful action, then the restricted action of S on α is faithful as well.

Русский

Если подмoноид S ⊆ M' действует на множества α фидельно, то ограниченное действие S на α тоже аккуратно верно (FaithfulSMul).

LaTeX

$$$ FaithfulSMul S α $$$

Lean4

@[to_additive]
instance faithfulSMul {M' α : Type*} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} [FaithfulSMul M' α] :
    FaithfulSMul S α :=
  ⟨fun h => Subtype.ext <| eq_of_smul_eq_smul h⟩

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