orderOf_dvd_natCard — Mathlib

English

For any finite group G and any element x ∈ G, the order of x divides the cardinality of G.

Русский

Пусть G — конечная группа и x ∈ G. Порядок элемента x делится кардинальностью группы: orderOf(x) делит card(G).

LaTeX

$$$\operatorname{orderOf}(x) \mid \lvert G \rvert$$$

Lean4

@[to_additive]
theorem orderOf_dvd_natCard {G : Type*} [Group G] (x : G) : orderOf x ∣ Nat.card G :=
  by
  obtain h | h := fintypeOrInfinite G
  · simp only [Nat.card_eq_fintype_card, orderOf_dvd_card]
  · simp only [card_eq_zero_of_infinite, dvd_zero]

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