mathlib
6075e179 - chore(ring_theory/roots_of_unity): golf some proofs (#17546)

Commit

3 years ago

chore(ring_theory/roots_of_unity): golf some proofs (#17546) Also add `is_primitive_root_of_mem_primitive_roots`: this implication doesn't need `k ≠ 0`.

Author

urkud

Parents

9c759b4c

mathlib 6075e179 - chore(ring_theory/roots_of_unity): golf some proofs (#17546)

mathlib
6075e179 - chore(ring_theory/roots_of_unity): golf some proofs (#17546)