Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-23 11:37 ddc016c6

View on Github →

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

Estimated changes

added theorem pow_lt_pow_of_lt_left
added theorem pow_right_inj
added def real.angle.angle
added theorem real.angle.coe_add
added theorem real.angle.coe_gsmul
added theorem real.angle.coe_neg
added theorem real.angle.coe_sub
added theorem real.angle.coe_two_pi
added theorem real.angle.coe_zero
added theorem real.angle.cos_sin_inj
added theorem real.cos_eq_zero_iff
added theorem real.cos_sub_cos
added theorem real.sin_sub_sin
added theorem complex.exp_nat_mul
added theorem real.exp_nat_mul