clearing denominators

Stream: Is there code for X?

[Jujian Zhang]

Given a finset of $R[\frac1f]$, do we have a lemma to clear their denominators, i.e.
Do we have the following:

import ring_theory.localization.basic
import ring_theory.graded_algebra.basic

section clear_denominator

variables (R : Type*) [comm_ring R] (f : R) [decidable_eq (localization.away f)]

lemma clear_denominator (s : finset (localization.away f)) :
  ∃ (n : ℕ), ∀ (x : localization.away f), x ∈ s →
    x * localization.mk (f^n) 1 ∈
    set.range (λ y, (localization.mk y 1 : localization.away f)) := sorry

end clear_denominator

If not, I will pr this and what should this lemma be called?

[Johan Commelin]

This generalises to arbitrary localisations, right?

[Johan Commelin]

Except that it will not be f^n, but some random product of denominators.

[Andrew Yang]

Stuff related to these are in file#ring_theory/localization/integer. I think you could probably fiddle with them and get what you want.

[Jujian Zhang]

Thanks! there is docs#is_localization.common_denom