instFaithfulSMul — Mathlib

English

For each i, the action of G_i on NormalWord d is faithful, i.e., different elements of G_i induce different endomorphisms of NormalWord d.

Русский

Для каждого i действие G_i на NormalWord d верно, то есть разные элементы G_i индуцируют разные эндоморфизмы NormalWord d.

LaTeX

$$$$\\text{For each } i,\\; \\text{the action } G_i \\curvearrowright \\mathrm{NormalWord}\, d \\text{ is faithful}.$$$$

Lean4

instance : FaithfulSMul (PushoutI φ) (NormalWord d) :=
  ⟨fun h => by simpa using congr_arg prod (h empty)⟩

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