formPerm_eq_self_of_notMem

Mathlib.GroupTheory.Perm.Cycle.Concrete

URI: https://scilib.ai/kg/mathlib#Cycle.formPerm_eq_self_of_notMem

← MathLib Explorer

English

If x is not in the cycle, formPerm s h x = x.

Русский

Если x не принадлежит циклу, то formPerm s h x = x.

LaTeX

$$$\\text{formPerm\_eq\_self\_of\_notMem}(s,h,x,hx) :\\quad \\text{formPerm } s h x = x$$$

Lean4

theorem formPerm_eq_self_of_notMem (s : Cycle α) (h : Nodup s) (x : α) (hx : x ∉ s) : formPerm s h x = x :=
  by
  induction s using Quot.inductionOn
  simpa using List.formPerm_apply_of_notMem hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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