Mathlib Map

Theorems · Definition · complex analysis

sineTerm

ℂ → ℕ → ℂ

The main term in the infinite product for sine.

Defined in
Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Cited by
10 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.

HasProdUniformlyOn_sineTerm_prod_on_compact · cited by 1HasProdUniformlyOn_sineTe…sineTerm_ne_zero · cited by 1sineTerm_ne_zeromultipliableUniformlyOn_euler_sin_prod_on_compact · cited by 1multipliableUniformlyOn_e…logDeriv_prod_sineTerm_eq_sum_cotTerm · cited by 1logDeriv_prod_sineTerm_eq…multipliable_sineTerm · cited by 1multipliable_sineTermlogDeriv_sineTerm_eq_cotTerm · cited by 1logDeriv_sineTerm_eq_cotT…tendsto_euler_sin_prod' · cited by 1tendsto_euler_sin_prod'euler_sineTerm_tprod · cited by 1euler_sineTerm_tprodtendsto_logDeriv_euler_sin_div · cited by 1tendsto_logDeriv_euler_si…HasProdLocallyUniformlyOn_euler_sin_prod · cited by 1HasProdLocallyUniformlyOn…Complex · cited by 5565ComplexsineTermCITED 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 by10

Results whose statement or proof uses this declaration.