Commit 2023-06-07 13:39 e7eeaa6f

View on Github →

feat: port RingTheory.RootsOfUnity.Complex (#4798)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RootsOfUnity/Complex.lean

added theorem Complex.card_primitiveRoots

added theorem Complex.card_rootsOfUnity

added theorem Complex.isPrimitiveRoot_exp

added theorem Complex.isPrimitiveRoot_exp_of_coprime

added theorem Complex.isPrimitiveRoot_iff

added theorem IsPrimitiveRoot.arg

added theorem IsPrimitiveRoot.arg_eq_pi_iff

added theorem IsPrimitiveRoot.arg_eq_zero_iff

added theorem IsPrimitiveRoot.arg_ext

added theorem IsPrimitiveRoot.nnnorm_eq_one

added theorem IsPrimitiveRoot.norm'_eq_one