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 →