Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-22 09:54 7a5fac38

View on Github →

feat(ring_theory/roots_of_unity): primitive root lemmas (#10356) From the flt-regular project.

Estimated changes

Modified src/ring_theory/roots_of_unity.lean

added theorem is_primitive_root.eq_order_of

added theorem is_primitive_root.map_iff_of_injective

added theorem is_primitive_root.map_of_injective

added theorem is_primitive_root.of_map_of_injective

added theorem is_primitive_root.of_subsingleton

added theorem is_primitive_root.unique

added theorem is_primitive_root.zero