Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_primitive_root.pow_of_dvd

Modification history

2021-12-28 03:25
src/ring_theory/roots_of_unity.lean
feat(ring_theory/polynomial/cyclotomic/basic): add cyclotomic_expand_eq_cyclotomic (#10974) …
Added is_primitive_root.pow_of_dvdView on Github →