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

Commit
6 years ago
feat(*): polar co-ordinates, de moivre, trig identities, quotient group for angles (#745) * feat(algebra/group_power): re-PRing polar co-ords * Update group_power.lean * feat(analysis/exponential): re-PRing polar stuff * feat(data.complex.exponential): re-PR polar stuff * fix(analysis.exponential): stylistic * fix(data.complex.exponential): stylistic * fix(analysis/exponential.lean): angle_eq_iff_two_pi_dvd_sub * fix(analysis/exponential): angle_eq_iff_two_pi_dvd_sub
Committer
Parents
Loading