card_zpowers_le

Mathlib.GroupTheory.OrderOfElement

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

← MathLib Explorer

English

If a^k = 1 with k > 0, then the order of zpowers a is at most k.

Русский

Если a^k = 1 и k > 0, то order zpowers(a) ≤ k.

LaTeX

$$card_zpowers : Fintype.card (Subgroup.zpowers a) ≤ k$$

Lean4

@[to_additive]
theorem card_zpowers_le (a : G) {k : ℕ} (k_pos : k ≠ 0) (ha : a ^ k = 1) : Fintype.card (Subgroup.zpowers a) ≤ k :=
  by
  rw [Fintype.card_zpowers]
  apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

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

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

Разделы

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

Аффилиация

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