Mathlib Map

Theorems · Definition · complex analysis

cotTerm

ℂ → ℕ → ℂ

The term in the infinite sum expansion of cot.

Defined in
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Cited by
12 results in Mathlib
Foundations
Depth 109 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

summable_cotTerm · cited by 2summable_cotTermiteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum · cited by 1iteratedDerivWithin_cot_s…logDeriv_prod_sineTerm_eq_sum_cotTerm · cited by 1logDeriv_prod_sineTerm_eq…logDeriv_sineTerm_eq_cotTerm · cited by 1logDeriv_sineTerm_eq_cotT…eqOn_iteratedDerivWithin_cotTerm_integerComplement · cited by 1eqOn_iteratedDerivWithin_…eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet · cited by 1eqOn_iteratedDerivWithin_…eqOn_iteratedDeriv_cotTerm · cited by 1eqOn_iteratedDeriv_cotTermtendsto_logDeriv_euler_cot_sub · cited by 1tendsto_logDeriv_euler_co…cotTerm_identity · cited by 1cotTerm_identitydifferentiableOn_iteratedDerivWithin_cotTerm · cited by 0differentiableOn_iterated…Summable_cotTerm · cited by 0Summable_cotTermsummableLocallyUniformlyOn_iteratedDerivWithin_cotTerm · cited by 0summableLocallyUniformlyO…Complex · cited by 5565ComplexcotTermCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Complexstatement and proof · cited by 5,565

Cited by12

Results whose statement or proof uses this declaration.