Theorems · Definition · order theory
SignType.sign
{α : Type u_1} → [Zero α] → [inst : Preorder α] → [DecidableLT α] → α →o SignTypeThe sign of an element is 1 if it's positive, -1 if negative, 0 otherwise.
- Defined in
- Mathlib.Data.Sign.Defs
- Cited by
- 128 results in Mathlib
- Foundations
- Depth 63 from the axioms, rests on 955 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroPreorderDecidableLT
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by132
Results whose statement or proof uses this declaration.
- Real.Angle.signproof · cited by 158
- sign_posstatement · cited by 49
- Real.Angle.sign_coe_pi_div_twoproof · cited by 48
- sign_negstatement · cited by 35
- sign_zerostatement · cited by 33
- Real.Angle.sign_negproof · cited by 15
- Polynomial.signVariationsproof · cited by 13
- sign_eq_one_iffstatement and proof · cited by 13
- sign_mulstatement and proof · cited by 11
- Left.sign_negstatement · cited by 9
- sign_eq_neg_one_iffstatement and proof · cited by 9
- Real.Angle.sign_zeroproof · cited by 9