\prod_p Z_p x (-1,1) is open in the adeles of the rationals

[kbuzzard]

I mean, I say \prod_p Z_p x (-1,1) but the truth is that it's actually

  ({f | ∀ (v : InfinitePlace ℚ), f v ∈ Metric.ball 0 1} ×ˢ
    {f |
      ∀ (v : IsDedekindDomain.HeightOneSpectrum (𝓞 ℚ)),
        ↑f v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v})

So this is: (1) binary product of open sets is open, (2) finite product of open sets is open (the infinite places) and (3) product of adicCompletionIntegers is open (the finite places).

This is in NumberField/AdeleRing.lean