I want to to add theorem Rat.den_eq_of_add_den_eq_one

Stream: mathlib4

[sinianluoye]

Recently, I encountered a question where I needed to prove the following lemma:

example {m n:ℚ} (h: (m + n).den = 1): m.den = n.den := by

It is so simple, but I couldn't find it in mathlib.

Can I create a PR to add it to the mathlib repo?

[Aaron Liu]

sure!

[Kenny Lau]

(deleted)

[sinianluoye]

created PR #27991