Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-10 22:38 08800bb7

View on Github →

feat(analysis/special/functions/trigonometric): complex trig and some even/odd lemmas (#5404) Complex (and some real) trigonometry lemmas, parity propositions, and some field algebra.

Estimated changes

added theorem div_add_one
added theorem div_add_same
added theorem div_sub_one
added theorem div_sub_same
added theorem one_add_div
added theorem one_sub_div
added theorem same_add_div
added theorem same_sub_div
added theorem eq_of_norm_sub_le_zero
modified theorem complex.exp_pi_mul_I
added theorem complex.tan_add'
added theorem complex.tan_add
added theorem complex.tan_add_mul_I
added theorem complex.tan_eq
added theorem complex.tan_int_mul_pi
added theorem complex.tan_two_mul
modified theorem real.pi_ne_zero
added theorem real.sin_ne_zero_iff
added theorem real.tan_add'
added theorem real.tan_add
added theorem real.tan_eq_zero_iff
added theorem real.tan_int_mul_pi
added theorem real.tan_ne_zero_iff
added theorem real.tan_two_mul
added theorem complex.cos_add_mul_I
added theorem complex.cos_eq
added theorem complex.cos_mul_I
added theorem complex.sin_add_mul_I
added theorem complex.sin_eq
added theorem complex.sin_mul_I
added theorem complex.tan_mul_I
added theorem complex.tanh_mul_I
added theorem int.even_iff_not_odd
added theorem int.even_or_odd'
added theorem int.even_or_odd
added theorem int.even_xor_odd'
added theorem int.even_xor_odd
added theorem int.not_odd_iff
added theorem nat.even_iff_not_odd
added theorem nat.even_or_odd'
added theorem nat.even_xor_odd'
added theorem nat.even_xor_odd
added theorem nat.not_odd_iff