Commit 2025-10-05 10:19 bfc2799b

chore(RingTheory/PrimitiveRoots): switch argument for isUnit from 0 < k to k ≠ 0 (#29988) Did not do this for all lemmas in IsPrimitiveRoot namespace which is still heterogeneous between

• NeZero k
• 0 < k
• k ≠ 0 Note: there will always be some mismatch in hypotheses, because core has lemmas about divisibility in 0 < k hypothesis form On the way to describing the torsion subgroup, as requested in #29517