Commit 2024-11-04 08:35 88fac4fd

chore: refactor roots of unity to avoid PNat (#18516) This is an attempt to refactor the definition of rootsOfUnity using a Nat instead of a PNat.

• In the definition of rootsOfUnity, we replace (n : ℕ+) by (n : ℕ). The definition does not require n to be nonzero; it gives that rootsOfUnity 0 M is the top subgroup of the unit group of M.
• For results that need a positive n, we replace (n : ℕ+) with (n : ℕ) [NeZero n] in the parameters. In this way, they transparently apply when a PNat is used for n since n gets coerced to Nat and an NeZero (n : ℕ) instance is available. The main benefit is that one no longer needs constructions like rootsOfUnity ⟨n, <proof that n is positive⟩) R when n is a natural number; one can simply use rootsOfUnity n R. (One may need to turn the positivity proof into an NeZero instance, however, if that is not available automatically.) In addition, the code in Mathlib.RingTheory.RootsOfUnity.Basic can be simplified a bit in places, e.g., x ^ (k : ℕ) can be replaced by x ^ k and ∃ (i : ℕ), i < k ∧ P i can be replaced by ∃ i < k, P i. One result (eq_pow_of_mem_rootsOfUnity'; it was translating between Nats and PNats) can be removed altogether. Since I was going through this file anyway, I took the opportunity to replace => by ↦ and to do some golfing as well. What this PR does not do is also refactoring cyclotomic extensions to not use (sets of) PNats. This is a more complex matter and requires more thought and discussion.