Commit 2022-01-28 16:51 d58ce5ac
View on Github →feat(number_theory/cyclotomic/zeta): add is_cyclotomic_extension.zeta (#11695)
We add is_cyclotomic_extension.zeta n A B: any primitive n-th root of unity in a cyclotomic extension.
From flt-regular.