isThreeCycle_sq

Mathlib.GroupTheory.Perm.Cycle.Type

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

← MathLib Explorer

English

If g is a three-cycle, then g^2 is also a three-cycle.

Русский

Если g — трёхцикл, то g^2 также трёхцикл.

LaTeX

$$If IsThreeCycle(g) then IsThreeCycle(g^2)$$

Lean4

theorem isThreeCycle_sq {g : Perm α} (ht : IsThreeCycle g) : IsThreeCycle (g * g) :=
  by
  rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
  rw [ht.orderOf]
  norm_num

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

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

Разделы

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

Аффилиация

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