mathlib

ff48cd59 - feat(ring_theory): fractions with integral denominator can be reduced