Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_primitive_root.aut_to_pow_spec

Modification history

2022-02-10 13:11
src/ring_theory/roots_of_unity.lean
feat(number_theory/cyclotomic/gal): the Galois group of K(ζₙ) (#11808) …
Added is_primitive_root.aut_to_pow_specView on Github →