isCycle_inv

Mathlib.GroupTheory.Perm.Cycle.Basic

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

English

A permutation is a cycle iff its inverse is a cycle.

Русский

Перестановка является циклом тогда и только тогда, когда её обратная — циклична.

LaTeX

$$IsCycle(f^{-1}) ⇔ IsCycle(f)$$

Lean4

@[simp]
theorem isCycle_inv : IsCycle f⁻¹ ↔ IsCycle f :=
  ⟨fun h => h.inv, IsCycle.inv⟩

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

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

Разделы

Аффилиация

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