inv_iff

Mathlib.GroupTheory.Perm.Cycle.Type

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

English

IsThreeCycle is preserved under taking inverses: IsThreeCycle f⁻¹ iff IsThreeCycle f.

Русский

IsThreeCycle сохраняется при взятии обратной перестановки: IsThreeCycle f⁻¹ ⇔ IsThreeCycle f.

LaTeX

$$@[simp] IsThreeCycle(f⁻¹) ↔ IsThreeCycle(f)$$

Lean4

@[simp]
theorem inv_iff {f : Perm α} : IsThreeCycle f⁻¹ ↔ IsThreeCycle f :=
  ⟨by
    rw [← inv_inv f]
    apply inv, inv⟩

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

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

Разделы

Аффилиация

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