cycleFactorsFinset_eq_singleton

Mathlib.GroupTheory.Perm.Cycle.Factors

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

← MathLib Explorer

English

For IsCycle, cycleFactorsFinset equals the singleton {f}.

Русский

Для IsCycle выполняется cycleFactorsFinset(f) = {f}.

LaTeX

$$$f.IsCycle \Rightarrow cycleFactorsFinset(f) = {f}$$$

Lean4

theorem cycleFactorsFinset_eq_singleton {f : Perm α} (hf : IsCycle f) : f.cycleFactorsFinset = { f } :=
  cycleFactorsFinset_eq_singleton_self_iff.mpr hf

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

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

Разделы

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

Аффилиация

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