nonempty

Mathlib.GroupTheory.Perm.Centralizer

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

← MathLib Explorer

English

For any finite α and g ∈ Sym(α), there exists a Basis g.

Русский

Для любой конечной α и g ∈ Sym(α) существует Basis g.

LaTeX

$$$\exists a: g.Basis$$$

Lean4

theorem nonempty (g : Perm α) : Nonempty (Basis g) :=
  by
  have (c : g.cycleFactorsFinset) : c.val.support.Nonempty :=
    IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp c.prop).1
  exact ⟨fun c ↦ (this c).choose, fun c ↦ (this c).choose_spec⟩

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

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

Разделы

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

Аффилиация

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