sameCycle_one

Mathlib.GroupTheory.Perm.Cycle.Basic

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

English

For the identity permutation id on α, two elements x and y satisfy SameCycle(id, x, y) if and only if x = y.

Русский

Для тzже перестановки-идентичности id на α, x и y лежат в одной и той же группе цикла id iff x = y.

LaTeX

$$\\forall x,y\\in\\alpha,\\ SameCycle(\\mathrm{id}_{\\alpha}) x y \\iff x = y.$$

Lean4

@[simp]
theorem sameCycle_one : SameCycle 1 x y ↔ x = y := by simp [SameCycle]

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

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

Разделы

Аффилиация

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