Finite products of basic opens in a prime spectrum

The basic open defined by a finite product of ring elements is the categorical product of their basic opens in the lattice of open subsets of the prime spectrum.

This is topological prime-spectrum infrastructure: its signature uses a commutative ring together with the opens of its prime spectrum and their categorical finite products, but no scheme.

theorem PrimeSpectrum.basicOpen_prod_eq_pi {R : CommRingCat} {α : Type u_1} [Fintype α] (g : α → ↑R) : basicOpen (∏ a : α, g a) = ∏ᶜ basicOpen ∘ g

The basic open of a finite product is the product of the corresponding basic opens.