mathlib3
feat(*): polar co-ordinates, de moivre, trig identities, quotient group for angles
#745

Merged

feat(*): polar co-ordinates, de moivre, trig identities, quotient group for angles #745

ChrisHughes24 merged 9 commits into master from polar

feat(algebra/group_power): re-PRing polar co-ords

3e82f73c

Update group_power.lean

b70f5f42

feat(analysis/exponential): re-PRing polar stuff

2412608b

feat(data.complex.exponential): re-PR polar stuff

6fc327fe

cipher1024 requested a review from

ChrisHughes24 6 years ago

cipher1024 requested a review from

johoelzl 6 years ago

cipher1024 assigned

ChrisHughes24 6 years ago

ChrisHughes24 commented on 2019-02-21

fix(analysis.exponential): stylistic

9a6941a7

fix(data.complex.exponential): stylistic

d4083014

fix(analysis/exponential.lean): angle_eq_iff_two_pi_dvd_sub

da7f42af

fix(analysis/exponential): angle_eq_iff_two_pi_dvd_sub

68ca7345

Merge branch 'master' into polar

ebda1e45

ChrisHughes24 merged ddc016c6 into master 6 years ago

ChrisHughes24 deleted the polar branch 6 years ago

Reviewers

ChrisHughes24

johoelzl

Assignees

ChrisHughes24

Labels

None yet

Milestone

No milestone