Commit 2023-01-17 10:40 86d0135d

View on Github →

feat: port Data.Real.Sign (#1618)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Real/Sign.lean

added theorem Real.inv_sign

added theorem Real.sign_apply_eq

added theorem Real.sign_apply_eq_of_ne_zero

added theorem Real.sign_eq_zero_iff

added theorem Real.sign_int_cast

added theorem Real.sign_inv

added theorem Real.sign_mul_nonneg

added theorem Real.sign_mul_pos_of_ne_zero

added theorem Real.sign_neg

added theorem Real.sign_of_neg

added theorem Real.sign_of_pos

added theorem Real.sign_one

added theorem Real.sign_zero