eq_of_left

Mathlib.GroupTheory.Perm.Cycle.Basic

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

English

If f x = x and x ~_f y, then x = y.

Русский

Если x фиксирована перестановкой f и x и y лежат в одном цикле f, то x = y.

LaTeX

$$$\\forall f:\\mathrm{Perm}(\\alpha),\\; \\forall x,y:\\alpha,\\mathrm{SameCycle}(f\\ x\\ y) \\Rightarrow IsFixedPt(f,x) \\Rightarrow x=y.$$$

Lean4

theorem eq_of_left (h : SameCycle f x y) (hx : IsFixedPt f x) : x = y :=
  let ⟨_, hn⟩ := h
  (hx.perm_zpow _).eq.symm.trans hn

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

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

Разделы

Аффилиация

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