faithfulSMul — Mathlib

English

The natural action of S on the ambient structure is faithful; equivalently, if g1,g2 ∈ S act identically on all elements of the target, then g1 = g2.

Русский

Естественное действие S на множество/модуль в окружении является верным, то есть если два элемента S действуют одинаково на все элементы модуля, то они равны.

LaTeX

$$$\forall g_1,g_2 \in S,\ (\forall x,\ g_1 \cdot x = g_2 \cdot x) \Rightarrow g_1 = g_2$$$

Lean4

scoped instance faithfulSMul :
    letI := (inclusion h).toModule;
    FaithfulSMul S T :=
  letI := (inclusion h).toModule
  ⟨fun {x y} h ↦ Subtype.ext <| by convert Subtype.ext_iff.mp (h 1) using 1 <;> exact (mul_one _).symm⟩

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