toPerm_injective — Mathlib

English

If the group action is faithful, the map a ↦ toPerm(a) is injective.

Русский

Если действие faithful, переход к перестановке по элементу группы инъективен.

LaTeX

$$$ \text{toPerm} : α \to \mathrm{Equiv.Perm}(β) \; \text{is injective under FaithfulSMul}$$$

Lean4

/-- `MulAction.toPerm` is injective on faithful actions. -/
@[to_additive /-- `AddAction.toPerm` is injective on faithful actions. -/
    ]
theorem toPerm_injective [FaithfulSMul α β] : Function.Injective (MulAction.toPerm : α → Equiv.Perm β) :=
  (show Function.Injective (Equiv.toFun ∘ MulAction.toPerm) from smul_left_injective').of_comp

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