HasEnoughRootsOfUnity ℤ 0 is true

Stream: mathlib4

[Jz Pan]

The following result sounds silly:

import Mathlib

example : HasEnoughRootsOfUnity ℤ 0 := by
  refine ⟨⟨2, by simp, fun n hn ↦ ?_⟩, ?_⟩
  · rw [zero_dvd_iff]
    norm_cast at hn
    rw [← pow_zero 2] at hn
    exact Nat.pow_right_injective le_rfl hn
  · rw [rootsOfUnity_zero, Subgroup.topEquiv.isCyclic]
    infer_instance

On the other hand, HasEnoughRootsOfUnity ℤ_[p] 0 is not true, since $\Z_p^\times$ is not a cyclic group, because its cardinality is $2^{\aleph_0}$ (which is not in mathlib yet).

The background is that I want to show HasEnoughRootsOfUnity ℤ_[p] n ↔ n ∣ (p ^ torsionfreeUnitsExponent p).totient, and I found that I need to exclude n = 0 case.

Maybe we should add a non-zero condition to HasEnoughRootsOfUnity to eliminate such silly things.

[Michael Stoll]

This comes from docs#IsPrimitiveRoot, where IsPrimitiveRoot x 0 is true for any element x of infinite order, together with rootsOfUnity 0 M = (⊤ : Subgroup Mˣ) (docs#rootsOfUnity).
So either all of these should be "fixed" to give something more sensible when n = 0, or you'll have to add the nonzero assumption where you need it.
I think we usually prefer to keep the definitions simple and add the conditions for the results where needed.