∀ (R : Type u_1) {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [NoZeroDivisors R]
  [alg : Algebra.IsAlgebraic R A] (s : Finset A), ∃ y, y ≠ 0 ∧ ∀ z ∈ s, IsIntegral R (y • z)