orderOf_dvd_of_mem_zpowers

Mathlib.GroupTheory.OrderOfElement

URI: https://scilib.ai/kg/mathlib#orderOf_dvd_of_mem_zpowers

← MathLib Explorer

English

If y lies in zpowers x, then orderOf y divides orderOf x.

Русский

Если y лежит в zpowers x, то orderOf y делит orderOf x.

LaTeX

$$orderOf(y) ∣ orderOf(x)$$

Lean4

@[to_additive]
theorem orderOf_dvd_of_mem_zpowers (h : y ∈ Subgroup.zpowers x) : orderOf y ∣ orderOf x :=
  by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
  rw [orderOf_dvd_iff_pow_eq_one]
  exact zpow_pow_orderOf

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

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

Разделы

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

Аффилиация

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