Documentation

Mathlib.Data.Real.Sign

Real sign function #

This file introduces and contains some results about Real.sign which maps negative real numbers to -1, positive real numbers to 1, and 0 to 0.

Main definitions #

Tags #

sign function

noncomputable def Real.sign (r : ) :

The sign function that maps negative real numbers to -1, positive numbers to 1, and 0 otherwise.

Equations
theorem Real.sign_of_neg {r : } (hr : r < 0) :
theorem Real.sign_of_pos {r : } (hr : 0 < r) :
@[simp]
@[simp]
theorem Real.sign_apply_eq_of_ne_zero (r : ) (h : r 0) :

This lemma is useful for working with ℝˣ

@[simp]
theorem Real.sign_eq_zero_iff {r : } :
Real.sign r = 0 r = 0
theorem Real.sign_mul_pos_of_ne_zero (r : ) (hr : r 0) :
0 < Real.sign r * r
@[simp]