norm_num yielding 1/1

Stream: mathlib4

[Thomas Murrills]

Just letting norm_num users know: if you encounter 1/1 in a norm_num call, e.g.

#norm_num (5 * 5⁻¹ : ℚ) -- 1/1

don't worry! We missed a prime on one of our definitions (.isRat vs. .isRat'). We'll bundle this fix into the ring functionality PR mathlib4#1711, which depends on it (and is almost done).