Theorems · Definition · complex analysis
Complex.arg
ℂ → ℝ
arg returns values in the range $(-π, π]$, such that for x ≠ 0,
sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs,
arg 0 defaults to 0
- Cited by
- 220 results in Mathlib
- Foundations
- Depth 187 from the axioms, rests on 4,712 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Norm.normproof · cited by 5,413
- Real.piproof · cited by 1,774
- Complex.reproof · cited by 882
- Complex.improof · cited by 591
- Real.arcsinproof · cited by 125
Cited by229
Results whose statement or proof uses this declaration.
- Orientation.oangleproof · cited by 205
- Complex.logproof · cited by 187
- Orientation.oangle_revproof · cited by 42
- Orientation.oangle_neg_orientation_eq_negproof · cited by 26
- Orientation.oangle_zero_leftproof · cited by 25
- polarCoordproof · cited by 25
- Complex.arg_zerostatement · cited by 22
- Orientation.oangle_zero_rightproof · cited by 22
- Orientation.oangle_selfproof · cited by 17
- Circle.angleDiffproof · cited by 17
- Complex.arg_ofReal_of_nonnegstatement · cited by 16
- Circle.pathproof · cited by 16
Showing the 200 most cited of 229.