This file defines the typeclass
IsROrC intended to have only two instances:
ℝ and ℂ. It is meant for definitions and theorems which hold for both the real and the complex case,
and in particular when the real case follows directly from the complex case by setting
im to zero and so on. Its API follows closely that of ℂ.
Applications include defining inner products and Hilbert spaces for both the real and complex case. One typically produces the definitions and proof for an arbitrary field of this typeclass, which basically amounts to doing the complex case, and the two cases then fall out immediately from the two instances of the class.
The instance for
ℝ is registered in this file.
The instance for
ℂ is declared in
Implementation notes #
The coercion from reals into an
IsROrC field is done by registering
CoeTC. For this to work, we must proceed carefully to avoid problems involving circular
coercions in the case
K=ℝ; in particular, we cannot use the plain
Coe and must set
priorities carefully. This problem was already solved for
ℕ, and we copy the solution detailed
Mathlib/Data/Nat/Cast/Defs.lean. See also Note [coercion into rings] for more details.
In addition, several lemmas need to be set at priority 900 to make sure that they do not override
their counterparts in
Mathlib/Analysis/Complex/Basic.lean (which causes linter errors).
A few lemmas requiring heavier imports are in
- norm : K → ℝ
- add : K → K → K
- zero : K
- nsmul : ℕ → K → K
- mul : K → K → K
- one : K
- natCast : ℕ → K
- npow : ℕ → K → K
- neg : K → K
- sub : K → K → K
- zsmul : ℤ → K → K
- intCast : ℤ → K
- inv : K → K
- div : K → K → K
- zpow : ℤ → K → K
- exists_pair_ne : ∃ x y, x ≠ y
- ratCast : ℚ → K
- qsmul : ℚ → K → K
- dist : K → K → ℝ
- edist : K → K → ENNReal
- toUniformSpace : UniformSpace K
- toBornology : Bornology K
- star : K → K
- star_involutive : Function.Involutive star
- smul : ℝ → K → K
- toFun : ℝ → K
- I : K
Imaginary unit in
K. Meant to be set to
K = ℝ.
- I_re_ax : ↑IsROrC.re IsROrC.I = 0
- toPartialOrder : PartialOrder K
only an instance in the
- toDecidableEq : DecidableEq K
This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.
Characteristic zero #
Cast lemmas #
Cauchy sequences #
z ≤ w iff
w - z is real and nonnegative,
ℂ are star ordered rings.
(That is, a star ring in which the nonnegative elements are those of the form
star z * z.)
Note this is only an instance with
open scoped ComplexOrder.