English
Let M be a submonoid of a commutative ring R and S a commutative R-algebra localized at M. For any finite index set ι and any family f: ι → S, there exists b ∈ M such that every (b in R) times f(i) is an integer (i.e., lies in the image of R in S).
Русский
Пусть M — подмономоды R, S — коммутативное R-алгебраическое кольцо, локализованное по M. Для конечного индекса ι и семейства f: ι → S существует b ∈ M такое, что каждый (b)·f(i) принадлежит образу R в S.
LaTeX
$$$\exists b \in M, \forall i, \ IsInteger_R( (b : R) \cdot f(i) )$$$
Lean4
/-- We can clear the denominators of a finite indexed family of fractions. -/
theorem exist_integer_multiples_of_finite {ι : Type*} [Finite ι] (f : ι → S) :
∃ b : M, ∀ i, IsLocalization.IsInteger R ((b : R) • f i) :=
by
cases nonempty_fintype ι
obtain ⟨b, hb⟩ := exist_integer_multiples M Finset.univ f
exact ⟨b, fun i => hb i (Finset.mem_univ _)⟩
