card_orderOf_eq_totient — Mathlib

English

In a finite cyclic group α, the exponent equals the cardinality: exponent α = |α|.

Русский

В конечной циклической группе α показатель степени равен кардиналу: экспонента α = |α|.

LaTeX

$$exponent α = Nat.card α$$

Lean4

@[to_additive]
theorem card_orderOf_eq_totient [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :
    #{a : α | orderOf a = d} = totient d := by
  classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd

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