Commit 2024-03-28 10:26 e18e9225

feat: characterize roots of unity in cyclotomic extensions (#10710) We add IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder: If x is a root of unity (spelled as IsOfFinOrder x) in an n-th cyclotomic extension of ℚ, where n is odd, and ζ is a primitive n-th root of unity, then there exists r < n such that x = ζ^r or x = -ζ^r. From flt-regular

• depends on: #11235