Commit 2023-06-06 20:29 03e1c2fa

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Arctan (#4750)

Estimated changes

Modified Mathlib.lean

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

added theorem Real.arccos_eq_arctan

added theorem Real.arcsin_eq_arctan

added theorem Real.arctan_eq_arccos

added theorem Real.arctan_eq_arcsin

added theorem Real.arctan_eq_of_tan_eq

added theorem Real.arctan_lt_pi_div_two

added theorem Real.arctan_mem_Ioo

added theorem Real.arctan_neg

added theorem Real.arctan_one

added theorem Real.arctan_tan

added theorem Real.arctan_zero

added theorem Real.coe_tanLocalHomeomorph

added theorem Real.coe_tanLocalHomeomorph_symm

added theorem Real.continuousAt_arctan

added theorem Real.continuousOn_tan

added theorem Real.continuousOn_tan_Ioo

added theorem Real.continuous_arctan

added theorem Real.continuous_tan

added theorem Real.cos_arctan

added theorem Real.cos_arctan_pos

added theorem Real.cos_sq_arctan

added theorem Real.image_tan_Ioo

added theorem Real.neg_pi_div_two_lt_arctan

added theorem Real.range_arctan

added theorem Real.sin_arctan

added theorem Real.surjOn_tan

added def Real.tanLocalHomeomorph

added def Real.tanOrderIso

added theorem Real.tan_add'

added theorem Real.tan_add

added theorem Real.tan_arctan

added theorem Real.tan_eq_zero_iff

added theorem Real.tan_int_mul_pi_div_two

added theorem Real.tan_ne_zero_iff

added theorem Real.tan_surjective

added theorem Real.tan_two_mul