Theorems · Definition · field theory
Complex.im
ℂ → ℝ
The imaginary part of a complex number.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 591 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by619
Results whose statement or proof uses this declaration.
- Complex.argproof · cited by 220
- UpperHalfPlane.improof · cited by 128
- Complex.mul_restatement · cited by 115
- Complex.slitPlaneproof · cited by 113
- Complex.mul_imstatement · cited by 107
- Complex.normSqproof · cited by 103
- Real.rpow_mulproof · cited by 67
- Complex.re_add_imstatement and proof · cited by 41
- Complex.reProdImproof · cited by 39
- Complex.norm_expproof · cited by 33
- Complex.continuous_imstatement · cited by 32
- Complex.extstatement and proof · cited by 28
Showing the 200 most cited of 619.