Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-10 13:11 66d9cc1c

View on Github →

feat(number_theory/cyclotomic/gal): the Galois group of K(ζₙ) (#11808) from flt-regular!

Estimated changes

Created src/number_theory/cyclotomic/gal.lean

added theorem is_cyclotomic_extension.aut_to_pow_injective

added theorem is_primitive_root.from_zeta_aut_spec

Modified src/ring_theory/roots_of_unity.lean

added theorem is_primitive_root.aut_to_pow_spec