English
The natural-cardinality of the nth roots of unity equals n: Nat.card (rootsOfUnity n M) = n.
Русский
Естественная кардинальность n-й группы корней единицы равна n: Nat.card (rootsOfUnity n M) = n.
LaTeX
$$natCard_rootsOfUnity: Nat.card (rootsOfUnity n M) = n$$
Lean4
/-- If `M` satisfies `HasEnoughRootsOfUnity`, then the group of `n`th roots of unity
in `M` (is cyclic and) has order `n`. -/
theorem natCard_rootsOfUnity (M : Type*) [CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n] :
Nat.card (rootsOfUnity n M) = n := by
obtain ⟨ζ, h⟩ := exists_primitiveRoot M n
rw [← IsCyclic.exponent_eq_card]
refine dvd_antisymm ?_ ?_
· exact Monoid.exponent_dvd_of_forall_pow_eq_one fun g ↦ OneMemClass.coe_eq_one.mp g.prop
· nth_rewrite 1 [h.eq_orderOf]
rw [← (h.isUnit NeZero.out).unit_spec, orderOf_units]
let ζ' : rootsOfUnity n M := ⟨(h.isUnit NeZero.out).unit, ?_⟩
· rw [← Subgroup.orderOf_mk]
exact Monoid.order_dvd_exponent ζ'
simp only [mem_rootsOfUnity]
rw [← Units.val_inj, Units.val_pow_eq_pow_val, IsUnit.unit_spec, h.pow_eq_one, Units.val_one]
