Theorems · Definition · field theory
Complex.I
ℂ
The imaginary unit.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 866 results in Mathlib
- Foundations
- Depth 86 from the axioms, rests on 1,593 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
Cited by912
Results whose statement or proof uses this declaration.
- Complex.cosproof · cited by 279
- Complex.sinproof · cited by 258
- Complex.logproof · cited by 187
- circleMapproof · cited by 117
- MeasureTheory.charFunproof · cited by 84
- Circle.expproof · cited by 73
- Complex.norm_Istatement · cited by 46
- Function.Periodic.qParamproof · cited by 42
- Complex.re_add_imstatement and proof · cited by 41
- Complex.I_sqstatement and proof · cited by 40
- Orientation.kahlerproof · cited by 39
- Complex.conj_Istatement · cited by 36
Showing the 200 most cited of 912.