mathlib3

5cc2dfdd - feat(*): add various results split out from proof of Gallagher's theorem (#17985)

feat(*): add various results split out from proof of Gallagher's theorem (#17985) This is a collection of tiny results that are not really related but I'm bundling them together in an effort to aid review.