Commit 2023-06-07 12:41 55822efb

View on Github →

feat: port RingTheory.RootsOfUnity.Basic (#4677)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RootsOfUnity/Basic.lean

added theorem IsPrimitiveRoot.autToPow_spec

added theorem IsPrimitiveRoot.card_nthRootsFinset

added theorem IsPrimitiveRoot.card_primitiveRoots

added theorem IsPrimitiveRoot.card_rootsOfUnity'

added theorem IsPrimitiveRoot.card_rootsOfUnity

added theorem IsPrimitiveRoot.coe_autToPow_apply

added theorem IsPrimitiveRoot.coe_submonoidClass_iff

added theorem IsPrimitiveRoot.coe_units_iff

added theorem IsPrimitiveRoot.disjoint

added theorem IsPrimitiveRoot.eq_neg_one_of_two_right

added theorem IsPrimitiveRoot.eq_orderOf

added theorem IsPrimitiveRoot.eq_pow_of_mem_rootsOfUnity

added theorem IsPrimitiveRoot.eq_pow_of_pow_eq_one

added theorem IsPrimitiveRoot.geom_sum_eq_zero

added theorem IsPrimitiveRoot.iff_def

added theorem IsPrimitiveRoot.inv

added theorem IsPrimitiveRoot.inv_iff

added theorem IsPrimitiveRoot.isPrimitiveRoot_iff'

added theorem IsPrimitiveRoot.isPrimitiveRoot_iff

added theorem IsPrimitiveRoot.isUnit

added theorem IsPrimitiveRoot.map_iff_of_injective

added theorem IsPrimitiveRoot.map_of_injective

added theorem IsPrimitiveRoot.mk_of_lt

added theorem IsPrimitiveRoot.ne_one

added theorem IsPrimitiveRoot.ne_zero'

added theorem IsPrimitiveRoot.neg_one

added theorem IsPrimitiveRoot.nthRoots_nodup

added theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots'

added theorem IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots

added theorem IsPrimitiveRoot.of_map_of_injective

added theorem IsPrimitiveRoot.of_subsingleton

added theorem IsPrimitiveRoot.one

added theorem IsPrimitiveRoot.one_right_iff

added theorem IsPrimitiveRoot.pow

added theorem IsPrimitiveRoot.pow_eq_one_iff_dvd

added theorem IsPrimitiveRoot.pow_iff_coprime

added theorem IsPrimitiveRoot.pow_inj

added theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt

added theorem IsPrimitiveRoot.pow_of_coprime

added theorem IsPrimitiveRoot.pow_of_dvd

added theorem IsPrimitiveRoot.pow_of_prime

added theorem IsPrimitiveRoot.pow_sub_one_eq

added theorem IsPrimitiveRoot.primitiveRoots_one

added def IsPrimitiveRoot.toRootsOfUnity

added theorem IsPrimitiveRoot.unique

added theorem IsPrimitiveRoot.zero

added def IsPrimitiveRoot.zmodEquivZpowers

added theorem IsPrimitiveRoot.zmodEquivZpowers_apply_coe_int

added theorem IsPrimitiveRoot.zmodEquivZpowers_apply_coe_nat

added theorem IsPrimitiveRoot.zmodEquivZpowers_symm_apply_pow'

added theorem IsPrimitiveRoot.zmodEquivZpowers_symm_apply_pow

added theorem IsPrimitiveRoot.zmodEquivZpowers_symm_apply_zpow'

added theorem IsPrimitiveRoot.zmodEquivZpowers_symm_apply_zpow

added theorem IsPrimitiveRoot.zpow_eq_one

added theorem IsPrimitiveRoot.zpow_eq_one_iff_dvd

added theorem IsPrimitiveRoot.zpow_of_gcd_eq_one

added theorem IsPrimitiveRoot.zpowers_eq

added structure IsPrimitiveRoot

added theorem RingEquiv.restrictRootsOfUnity_coe_apply

added theorem RingEquiv.restrictRootsOfUnity_symm

added theorem card_rootsOfUnity

added theorem isPrimitiveRoot_of_mem_primitiveRoots

added theorem map_rootsOfUnity

added theorem map_rootsOfUnity_eq_pow_self

added theorem mem_primitiveRoots

added theorem mem_rootsOfUnity'

added theorem mem_rootsOfUnity

added theorem mem_rootsOfUnity_iff_mem_nthRoots

added theorem mem_rootsOfUnity_prime_pow_mul_iff'

added theorem mem_rootsOfUnity_prime_pow_mul_iff

added def primitiveRoots

added theorem primitiveRoots_zero

added def restrictRootsOfUnity

added theorem restrictRootsOfUnity_coe_apply

added theorem rootsOfUnity.coe_injective

added theorem rootsOfUnity.coe_mkOfPowEq

added theorem rootsOfUnity.coe_pow

added def rootsOfUnity.mkOfPowEq

added def rootsOfUnity

added def rootsOfUnityEquivNthRoots

added theorem rootsOfUnityEquivNthRoots_apply

added theorem rootsOfUnityEquivNthRoots_symm_apply

added theorem rootsOfUnity_le_of_dvd