feat(ring_theory/localization): generalize `exist_integer_multiples` to finite families (#9859)
feat(ring_theory/localization): generalize `exist_integer_multiples` to finite families (#9859)

This PR shows we can clear denominators of finitely-indexed collections of fractions (i.e. elements of `S` where `is_localization M S`), with the existing result about finite sets of fractions as a special case.







leanprover-community/mathlib,leanprover-community/mathlib