mathlib

6666ba2f - fix(real/sign): make `real.sign 0 = 0` to match `int.sign 0` (#8080)

fix(real/sign): make `real.sign 0 = 0` to match `int.sign 0` (#8080) Previously `sign 0 = 1` which is quite an unusual definition. This definition brings things in line with `int.sign`, and include a proof of this fact. A future refactor could probably introduce a sign for all rings with a partial order