Commit 2021-10-23 08:22 a75f7623

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.