natCard_powers_le_orderOf — Mathlib

English

If a has finite order, then the set of its powers is finite and its size does not exceed the order of a.

Русский

Пусть a имеет конечный порядок. Тогда множество степеней a конечно, и его размер не превосходит orderOf(a).

LaTeX

$$$|\mathrm{powers}(a)| \le \operatorname{orderOf}(a)$$$

Lean4

@[to_additive]
theorem natCard_powers_le_orderOf (ha : IsOfFinOrder a) : Nat.card (powers a : Set G) ≤ orderOf a := by
  classical
    simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range] using
    Finset.card_image_le (s := Finset.range (orderOf a))

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