Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-18 01:15 32258e92

View on Github →

chore(number_theory/cyclotomic/primitive_roots): generalisation linter (#16013)

Estimated changes

Modified src/number_theory/cyclotomic/primitive_roots.lean

modified theorem is_primitive_root.norm_eq_neg_one_pow

modified theorem is_primitive_root.norm_eq_one

modified theorem is_primitive_root.norm_of_cyclotomic_irreducible