English
If M has HasEnoughRootsOfUnity, then the group of nth roots of unity in M is finite.
Русский
Если M удовлетворяет HasEnoughRootsOfUnity, тогда группа n-й корней единицы в M конечна.
LaTeX
$$finite_rootsOfUnity: Finite (rootsOfUnity n M)$$
Lean4
/-- If `M` satisfies `HasEnoughRootsOfUnity`, then the group of `n`th roots of unity
in `M` is finite. -/
instance finite_rootsOfUnity (M : Type*) [CommMonoid M] (n : ℕ) [NeZero n] [HasEnoughRootsOfUnity M n] :
Finite <| rootsOfUnity n M := by
have := rootsOfUnity_isCyclic M n
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := rootsOfUnity n M)
have hg' : g ^ n = 1 := OneMemClass.coe_eq_one.mp g.prop
let f (j : ZMod n) : rootsOfUnity n M := g ^ (j.val : ℤ)
refine Finite.of_surjective f fun x ↦ ?_
obtain ⟨k, hk⟩ := Subgroup.mem_zpowers_iff.mp <| hg x
refine ⟨k, ?_⟩
simpa only [ZMod.natCast_val, ← hk, f, ZMod.coe_intCast] using (zpow_eq_zpow_emod' k hg').symm
