English
For a finite index set, there exists a common M-multiple making all corresponding fractions integers.
Русский
Для конечного множества индексов существует общий множитель M, делающий все соответствующие дроби целыми.
LaTeX
$$exist_integer_multiples(s,f)$$
Lean4
/-- We can clear the denominators of a `Finset`-indexed family of fractions. -/
theorem exist_integer_multiples {ι : Type*} (s : Finset ι) (f : ι → S) :
∃ b : M, ∀ i ∈ s, IsLocalization.IsInteger R ((b : R) • f i) :=
by
haveI := Classical.propDecidable
refine ⟨∏ i ∈ s, (sec M (f i)).2, fun i hi => ⟨?_, ?_⟩⟩
· exact (∏ j ∈ s.erase i, (sec M (f j)).2) * (sec M (f i)).1
rw [RingHom.map_mul, sec_spec', ← mul_assoc, ← (algebraMap R S).map_mul, ← Algebra.smul_def]
congr 2
refine _root_.trans ?_ (map_prod (Submonoid.subtype M) _ _).symm
rw [mul_comm, Submonoid.coe_finset_prod,
-- Porting note: explicitly supplied `f`
← Finset.prod_insert (f := fun i => ((sec M (f i)).snd : R)) (s.notMem_erase i), Finset.insert_erase hi]
rfl
