Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-05 05:24 08cdf37c

View on Github →

feat(analysis/complex/roots_of_unity): complex (primitive) roots of unity (#4330)

Estimated changes

Modified docs/undergrad.yaml

Created src/analysis/complex/roots_of_unity.lean

added theorem complex.card_primitive_roots

added theorem complex.card_roots_of_unity

added theorem complex.is_primitive_root_exp

added theorem complex.is_primitive_root_exp_of_coprime

added theorem complex.is_primitive_root_iff

added theorem complex.mem_roots_of_unity

Modified src/analysis/special_functions/trigonometric.lean

added theorem complex.two_pi_I_ne_zero

added theorem real.pi_ne_zero