Commit 2022-11-15 08:58 6075e179

View on Github →

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.

Estimated changes

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/roots_of_unity.lean

deleted theorem is_primitive_root.primitive_roots_zero

added theorem is_primitive_root_of_mem_primitive_roots

added theorem primitive_roots_zero