English
The subgroup of powers of a primitive root equals the set of k-th roots of unity.
Русский
Подмножество степеней примитивного корня совпадает с множеством k-й корней единицы.
LaTeX
$$Subgroup.zpowers ζ = rootsOfUnity k R$$
Lean4
theorem zpowers_eq {k : ℕ} [NeZero k] {ζ : Rˣ} (h : IsPrimitiveRoot ζ k) : Subgroup.zpowers ζ = rootsOfUnity k R :=
by
apply SetLike.coe_injective
have F : Fintype (Subgroup.zpowers ζ) := Fintype.ofEquiv _ h.zmodEquivZPowers.toEquiv
refine
@Set.eq_of_subset_of_card_le Rˣ _ _ F (rootsOfUnity.fintype R k)
(Subgroup.zpowers_le_of_mem <| show ζ ∈ rootsOfUnity k R from h.pow_eq_one) ?_
calc
Fintype.card (rootsOfUnity k R) ≤ k := card_rootsOfUnity R k
_ = Fintype.card (ZMod k) := (ZMod.card k).symm
_ = Fintype.card (Subgroup.zpowers ζ) := Fintype.card_congr h.zmodEquivZPowers.toEquiv
