Theorems · Definition · field theory
Complex.ofReal
ℝ → ℂ
The natural inclusion of the real numbers into the complex numbers.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 1,654 results in Mathlib
- Foundations
- Depth 86 from the axioms, rests on 1,589 definitions · uses propext, Classical.choice, Quot.sound
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 by1,729
Results whose statement or proof uses this declaration.
- Real.expproof · cited by 871
- Real.cosproof · cited by 424
- Real.sinproof · cited by 389
- Complex.logproof · cited by 187
- Complex.ofReal_mulstatement · cited by 180
- Real.sinhproof · cited by 142
- Complex.ofReal_negstatement · cited by 130
- Real.coshproof · cited by 119
- circleMapproof · cited by 117
- Real.rpow_oneproof · cited by 114
- Complex.continuous_ofRealstatement · cited by 107
- Complex.norm_realstatement and proof · cited by 105
Showing the 200 most cited of 1,729.