∀ {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Ring (κ i)]
  [inst_2 : (i : ι) → Algebra R (κ i)] (a : (i : ι) → κ i), spectrum R a = ⋃ i, spectrum R (a i)