mathlib

a1ddb551 - feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part a) (#18282)

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part a) (#18282) This adds the first half of the proof of Euler's infinite product, writing `sin (π * z) / (π * z)` as the first n terms of the product times a ratio of cosine integrals. (The second half will be to show that this ratio of cosine integrals tends to 1).