mathlib

6d90d35f - feat(analysis/fourier): monomials on the circle are orthonormal (#6952)

feat(analysis/fourier): monomials on the circle are orthonormal (#6952) Make the circle into a measure space, using Haar measure, and prove that the monomials `z ^ n` are orthonormal when considered as elements of L^2 on the circle.