Weak approximation at infinite places

[smmercuri]

This PR contains three weak approximation results of a number field K with respect to its infinite places of the following form

• K is dense in Π v, K
• K is dense in the infinite adele ring
• K is dense in any sub-collection Π {v // p v}, K of infinite place completions

Depends on #321
Depends on #322

[smmercuri]

Breaking this up into smaller PRs as it's too big!

Please review #321 and #322 first and then this one will become much smaller.

[kbuzzard]

I merged them!

[kbuzzard]

Let me know if this is ready. So you say you can't remove the awaiting-author label? Are you able to add more labels? If not, I wonder how this kind of basic communication between author and reviewer is supposed to work. In mathlib we have this nonstandard setup where every contributor gets write access to non-master branches and there it seems that everyone can edit labels.

Is the idea that I'm just supposed to be up to date with my github notifications I wonder?

[smmercuri]

Yeah this PR is now updated and ready to review. I can't edit labels at all, for mathlib PRs there's a cog next to the labels which let's me modify them but that cog doesn't appear here. From here it seems I'd be able to edit labels if I had "triage access"