Mathlib v3 is deprecated. Go to Mathlib v4

Theorem euler_sine.tendsto_integral_cos_pow_mul_div

Modification history

2023-02-01 07:41
src/analysis/special_functions/trigonometric/euler_sine_prod.lean
feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)
Added euler_sine.tendsto_integral_cos_pow_mul_divView on Github →