dvd_of_mem_cycleType

Mathlib.GroupTheory.Perm.Cycle.Type

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

English

If n is in the cycle-type of σ, then n divides the order of σ.

Русский

Если n принадлежит cycleType(σ), то n делится на порядок σ.

LaTeX

$$$$\text{If } n \in \mathrm{cycleType}(\sigma) \text{ then } n \mid \mathrm{orderOf}(\sigma).$$$$

Lean4

theorem dvd_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : n ∣ orderOf σ :=
  by
  rw [← lcm_cycleType]
  exact dvd_lcm h

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

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

Разделы

Аффилиация

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