Commit 2024-02-13 23:17 b4adfe72

View on Github →

feat: arctangent addition and Machin's formula for π (#9847) four_mul_arctan_inv_5_sub_arctan_inv_239 is theorem 1 in my own #6091.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

added theorem Real.arctan_add

added theorem Real.arctan_add_arctan_lt_pi_div_two

added theorem Real.arctan_add_eq_add_pi

added theorem Real.arctan_add_eq_sub_pi

added theorem Real.arctan_inv_2_add_arctan_inv_3

added theorem Real.arctan_inv_of_neg

added theorem Real.arctan_inv_of_pos

added theorem Real.arctan_ne_mul_pi_div_two

added theorem Real.four_mul_arctan_inv_5_sub_arctan_inv_239

added theorem Real.two_mul_arctan

added theorem Real.two_mul_arctan_add_pi

added theorem Real.two_mul_arctan_inv_2_sub_arctan_inv_7

added theorem Real.two_mul_arctan_inv_3_add_arctan_inv_7

added theorem Real.two_mul_arctan_sub_pi

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

added theorem Real.tan_pi_div_six

added theorem Real.tan_pi_div_three