mathlib3

980755c3 - feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)