Theorems · Inductive type · field theory
Complex
Type
Complex numbers consist of two Reals: a real part re and an imaginary part im.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 5,565 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 by6,123
Results whose statement or proof uses this declaration.
- Complex.ofRealstatement · cited by 1,654
- Complex.restatement and proof · cited by 882
- Complex.Istatement · cited by 866
- Complex.expstatement · cited by 612
- NumberField.InfinitePlaceproof · cited by 604
- Complex.imstatement and proof · cited by 591
- NumberField.InfinitePlace.IsRealproof · cited by 301
- UpperHalfPlane.coestatement · cited by 288
- Complex.cosstatement and proof · cited by 279
- NumberField.InfinitePlace.IsComplexproof · cited by 272
- Complex.sinstatement and proof · cited by 258
- NumberField.mixedEmbedding.mixedSpaceproof · cited by 239
Showing the 200 most cited of 6,123.