Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 18:49 cea5e4bb

View on Github →

feat(data/sign): the sign function (#12835)

Estimated changes

added def sign
added theorem sign_apply
added theorem sign_eq_zero_iff
added def sign_hom
added theorem sign_ne_zero
added theorem sign_neg
added theorem sign_pos
added def sign_type.cast
added theorem sign_type.cast_eq_coe
added theorem sign_type.coe_neg_one
added theorem sign_type.coe_one
added theorem sign_type.coe_zero
added inductive sign_type.le
added def sign_type.mul
added theorem sign_type.pos_eq_one
added theorem sign_type.zero_eq_zero
added inductive sign_type
added theorem sign_zero