Theorems · Theorem · complex analysis
cot_pi_mul_contDiffWithinAt
∀ {x : ℂ} (k : ℕ∞),
x ∈ Complex.integerComplement →
ContDiffWithinAt ℂ (↑k) (fun x => (↑Real.pi * x).cot) UpperHalfPlane.upperHalfPlaneSet x- Cited by
- 0 results in Mathlib
- Foundations
- Depth 202 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Complexstatement and proof · cited by 5,565
- ENatstatement and proof · cited by 4,985
- Real.pistatement · cited by 1,774
- Complex.ofRealstatement · cited by 1,654
- WithTop.somestatement · cited by 1,128
- ContDiffWithinAtstatement · cited by 283
- Complex.integerComplementstatement and proof · cited by 30
- UpperHalfPlane.upperHalfPlaneSetstatement · cited by 25
- Complex.cotstatement · cited by 19
- contDiffWithinAt_idproof · cited by 12
- contDiffWithinAt_constproof · cited by 9
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.