Theorems · Inductive type · order theory
SignType
Type
The type of signs.
- Defined in
- Mathlib.Data.Sign.Defs
- Cited by
- 318 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by343
Results whose statement or proof uses this declaration.
- Real.Angle.signstatement · cited by 158
- SignType.signstatement · cited by 128
- SignType.caststatement and proof · cited by 76
- sign_posstatement and proof · cited by 49
- Real.Angle.sign_coe_pi_div_twostatement and proof · cited by 48
- sign_negstatement and proof · cited by 35
- sign_zerostatement · cited by 33
- EuclideanGeometry.oangle_rotate_signstatement and proof · cited by 27
- Orientation.oangle_eq_angle_of_sign_eq_onestatement and proof · cited by 25
- EuclideanGeometry.oangle_eq_angle_of_sign_eq_onestatement · cited by 24
- SignType.coe_negstatement and proof · cited by 19
- Real.Angle.sign_negstatement · cited by 15
Showing the 200 most cited of 343.