applyFaithfulSMul

Mathlib.Algebra.Group.Action.End

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.applyFaithfulSMul

English

The action of Perm α on α is faithful: if f • a = g • a for all a, then f = g.

Русский

Действие Perm α на α верно: если f • a = g • a для всех a, то f = g.

LaTeX

$$$ \text{FaithfulSMul } (\mathrm{Perm}(\alpha)) \ α$$$

Lean4

/-- `Equiv.Perm.applyMulAction` is faithful. -/
instance applyFaithfulSMul (α : Type*) : FaithfulSMul (Perm α) α :=
  ⟨Equiv.ext⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru