∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] {ι : Type u_4} [Finite ι] (f : ι → S),
  ∃ b, ∀ (i : ι), IsLocalization.IsInteger R (↑b • f i)