Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_primitive_root.aut_to_pow_injective

Modification history

2022-02-10 23:42

src/number_theory/cyclotomic/gal.lean

chore(number_theory/cyclotomic/zeta): generalize to primitive roots (#11941) …

Added is_primitive_root.aut_to_pow_injective View on Github →