Complementary arctangents at the corners of a rectangle

Mathlib's Real.arctan_inv_of_pos gives arctan x⁻¹ = π / 2 - arctan x; the quotient form arctan (u / v) + arctan (v / u) = π / 2 that occurs when the two legs of a right angle are named separately is not stated there.

Main results

• Real.arctan_div_add_arctan_div: the quotient form of the complementary-angle law.
• TauCeti.arctan_corner_sum_eq_two_mul_pi_mul_I: the four corner angles of a rectangle straddling the imaginary axis sum to a full turn.

theorem Real.arctan_div_add_arctan_div {u v : ℝ} (hu : 0 < u) (hv : 0 < v) : arctan (u / v) + arctan (v / u) = Real.pi / 2

Complementary angles, in quotient form. For positive u and v the angles arctan (u / v) and arctan (v / u) are complementary.

theorem TauCeti.arctan_corner_sum_eq_two_mul_pi_mul_I {c B T : ℝ} (hc : 0 < c) (hB : 0 < B) (hT : 0 < T) : 2 * Complex.I * (↑(Real.arctan (c / T)) - ↑(Real.arctan (-B / T))) + Complex.I * (2 * ↑(Real.arctan (T / c))) - Complex.I * (2 * ↑(Real.arctan (T / -B))) = 2 * ↑Real.pi * Complex.I

The corner angles of a rectangle sum to a full turn. For a rectangle with vertical sides at -B < 0 < c and horizontal sides at heights ±T, the four angles subtended at the origin combine to 2π i.