The sign as a quotient by the absolute value #
In a linearly ordered division ring, the sign of x is x / |x|. This is the division form of
Mathlib's sign_mul_abs, and it holds at 0 too, since both sides vanish there.
Main results #
TauCeti.sign_eq_div_abs:sign x = x / |x|.
theorem
TauCeti.sign_eq_div_abs
{α : Type u_1}
[DivisionRing α]
[LinearOrder α]
[IsStrictOrderedRing α]
(x : α)
:
In a linearly ordered division ring, the sign of x is x / |x|.