Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 22:07 e690875d

View on Github →

chore(ring_theory/roots_of_unity): generalise (#13261)

Estimated changes

Modified src/ring_theory/roots_of_unity.lean

modified theorem is_primitive_root.eq_neg_one_of_two_right

modified theorem is_primitive_root.mem_roots_of_unity

modified theorem is_primitive_root.pow

modified theorem roots_of_unity.coe_pow