Theorems · Theorem · complex analysis
Complex.abs_arg_le_pi
∀ (z : ℂ), |z.arg| ≤ Real.pi
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- LT.lt.leproof · cited by 2,189
- absstatement · cited by 1,814
- Real.pistatement · cited by 1,774
- Complex.argstatement · cited by 220
- abs_leproof · cited by 64
- Complex.arg_le_piproof · cited by 8
- Complex.neg_pi_lt_argproof · cited by 7
Cited by3
Results whose statement or proof uses this declaration.
- Complex.angle_eq_abs_argproof · cited by 4
- Unitary.norm_argSelfAdjoint_le_piproof · cited by 3
- Complex.isTheta_exp_arg_mul_improof · cited by 2