Theorems · Theorem · real analysis
Real.arctan_add_eq_add_pi
∀ {x y : ℝ}, 1 < x * y → 0 < x → Real.arctan x + Real.arctan y = Real.arctan ((x + y) / (1 - x * y)) + Real.pi- Cited by
- 2 results in Mathlib
- Foundations
- Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Real.pistatement and proof · cited by 1,774
- add_commproof · cited by 1,535
- sub_eq_add_negproof · cited by 1,023
- zero_lt_oneproof · cited by 598
- LT.lt.transproof · cited by 370
- Real.arctanstatement and proof · cited by 111
- sub_eq_iff_eq_addproof · cited by 74
- mul_invproof · cited by 50
- sub_eq_iff_eq_add'proof · cited by 33
- inv_lt_one_of_one_lt₀proof · cited by 20
- LT.lt.asymmproof · cited by 10
Cited by2
Results whose statement or proof uses this declaration.
- Real.arctan_add_eq_sub_piproof · cited by 1
- Real.two_mul_arctan_add_piproof · cited by 0