Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-02 10:14 8876ba25

View on Github →

feat(ring_theory/roots_of_unity): (primitive) roots of unity (#4260)

Estimated changes

Created src/ring_theory/roots_of_unity.lean

added theorem card_roots_of_unity

added theorem is_primitive_root.card_primitive_roots

added theorem is_primitive_root.card_roots_of_unity'

added theorem is_primitive_root.card_roots_of_unity

added theorem is_primitive_root.coe_subgroup_iff

added theorem is_primitive_root.coe_units_iff

added theorem is_primitive_root.eq_neg_one_of_two_right

added theorem is_primitive_root.eq_pow_of_mem_roots_of_unity

added theorem is_primitive_root.eq_pow_of_pow_eq_one

added theorem is_primitive_root.fpow_eq_one

added theorem is_primitive_root.fpow_eq_one_iff_dvd

added theorem is_primitive_root.fpow_of_gcd_eq_one

added theorem is_primitive_root.gpow_eq_one

added theorem is_primitive_root.gpow_eq_one_iff_dvd

added theorem is_primitive_root.gpow_of_gcd_eq_one

added theorem is_primitive_root.gpowers_eq

added theorem is_primitive_root.iff_def

added theorem is_primitive_root.inv'

added theorem is_primitive_root.inv

added theorem is_primitive_root.inv_iff'

added theorem is_primitive_root.inv_iff

added theorem is_primitive_root.is_primitive_root_iff'

added theorem is_primitive_root.is_primitive_root_iff

added theorem is_primitive_root.is_unit

added theorem is_primitive_root.mem_roots_of_unity

added theorem is_primitive_root.mk_of_lt

added theorem is_primitive_root.neg_one

added theorem is_primitive_root.one

added theorem is_primitive_root.one_right_iff

added theorem is_primitive_root.pow_eq_one_iff_dvd

added theorem is_primitive_root.pow_iff_coprime

added theorem is_primitive_root.pow_inj

added theorem is_primitive_root.pow_ne_one_of_pos_of_lt

added theorem is_primitive_root.pow_of_coprime

added def is_primitive_root.zmod_equiv_gpowers

added theorem is_primitive_root.zmod_equiv_gpowers_apply_coe_int

added theorem is_primitive_root.zmod_equiv_gpowers_apply_coe_nat

added theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_gpow'

added theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_gpow

added theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_pow'

added theorem is_primitive_root.zmod_equiv_gpowers_symm_apply_pow

added structure is_primitive_root

added theorem map_roots_of_unity

added theorem mem_primitive_roots

added theorem mem_roots_of_unity

added theorem mem_roots_of_unity_iff_mem_nth_roots

added def primitive_roots

added def roots_of_unity

added def roots_of_unity_equiv_nth_roots

added theorem roots_of_unity_equiv_nth_roots_apply

added theorem roots_of_unity_equiv_nth_roots_symm_apply

added theorem roots_of_unity_le_of_dvd