mathlib3

570e9f48 - feat(ring_theory/localization/away) : Add `num_denom` section (#18830)

feat(ring_theory/localization/away) : Add `num_denom` section (#18830) Added a section `num_denom`: the main result is the lemma `exists_reduced_fraction` that shows that every non-zero element `b` in a `localization.away x` of a UFM can be written in a unique way as `b=x^n * a` with `n : ℤ` and `a` not divisible by `x`. Co-authored-by: Vierkantor <vierkantor@vierkantor.com>