exponent_eq_card — Mathlib

English

In a finite cyclic group α, exponent α equals card α.

Русский

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

LaTeX

$$exponent α = Nat.card α$$

Lean4

@[to_additive]
theorem exponent_eq_card [Group α] [IsCyclic α] : exponent α = Nat.card α :=
  by
  obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)
  apply Nat.dvd_antisymm Group.exponent_dvd_nat_card
  rw [← hg]
  exact order_dvd_exponent _

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