Theorem IsPrimitiveRoot.geom_sum_isUnit'

Modification history

2025-10-15 16:18
Mathlib/RingTheory/RootsOfUnity/CyclotomicUnits.lean
feat: add Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits (#30085) …
Added IsPrimitiveRoot.geom_sum_isUnit'View on Github →