Zulip Chat Archive

Stream: mathlib4

Topic: norm_num yielding 1/1


Thomas Murrills (Jan 21 2023 at 03:08):

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).


Last updated: Dec 20 2023 at 11:08 UTC