orbit_eq_top

Mathlib.GroupTheory.Sylow

URI: https://scilib.ai/kg/mathlib#Sylow.orbit_eq_top

English

The G-orbit of P in Sylow_p(G) is the whole set; i.e., orbit_G(P) = ⊤.

Русский

Орбитa G над P вSylow_p(G) равна всему множеству; то есть orbit_G(P) = ⊤.

LaTeX

$$$\\mathrm{orbit}_G(P) = \\top$. $$

Lean4

@[simp]
theorem orbit_eq_top [Fact p.Prime] [Finite (Sylow p G)] (P : Sylow p G) : orbit G P = ⊤ :=
  top_le_iff.mp fun Q _ => exists_smul_eq G P Q

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

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

Разделы

Аффилиация

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