orderOf_eq_card_of_forall_mem_zpowers

Mathlib.GroupTheory.SpecificGroups.Cyclic

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

← MathLib Explorer

English

If every element x of α lies in zpowers g, then orderOf g equals card α.

Русский

Если каждый элемент α лежит в zpowers g, то orderOf g = card α.

LaTeX

$$orderOf g = Nat.card α, если ∀ x, x ∈ zpowers g$$

Lean4

@[to_additive]
theorem orderOf_eq_card_of_forall_mem_zpowers {g : α} (hx : ∀ x, x ∈ zpowers g) : orderOf g = Nat.card α := by
  rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]

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

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

Разделы

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

Аффилиация

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