Theorems · Theorem · real analysis
Real.tan_add
∀ {x y : ℝ},
(((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨
(∃ k, x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ l, y = (2 * ↑l + 1) * Real.pi / 2) →
Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- Complexproof · cited by 5,565
- Nat.cast_oneproof · cited by 2,501
- Real.pistatement and proof · cited by 1,774
- Complex.ofRealproof · cited by 1,654
- Int.cast_oneproof · cited by 371
- Complex.ofReal_mulproof · cited by 180
- Int.cast_addproof · cited by 124
- Int.cast_mulproof · cited by 113
- Real.tanstatement and proof · cited by 100
- Complex.ofReal_addproof · cited by 94
- Int.cast_ofNatproof · cited by 86
Cited by1
Results whose statement or proof uses this declaration.
- Real.tan_add'proof · cited by 1