# Normed space structure on `ℂ`. #

This file gathers basic facts of analytic nature on the complex numbers.

## Main results #

This file registers `ℂ` as a normed field, expresses basic properties of the norm, and gives tools on the real vector space structure of `ℂ`. Notably, it defines the following functions in the namespace `Complex`.

Name | Type | Description
--- | --- | ---
`equivRealProdCLM` | ℂ ≃L[ℝ] ℝ × ℝ | The natural `ContinuousLinearEquiv` from `ℂ` to `ℝ × ℝ`
`reCLM` | ℂ →L[ℝ] ℝ | Real part function as a `ContinuousLinearMap`
`imCLM` | ℂ →L[ℝ] ℝ | Imaginary part function as a `ContinuousLinearMap`
`ofRealCLM` | ℝ →L[ℝ] ℂ | Embedding of the reals as a `ContinuousLinearMap`
`ofRealLI` | ℝ →ₗᵢ[ℝ] ℂ | Embedding of the reals as a `LinearIsometry`
`conjCLE` | ℂ ≃L[ℝ] ℂ | Complex conjugation as a `ContinuousLinearEquiv`
`conjLIE` | ℂ ≃ₗᵢ[ℝ] ℂ | Complex conjugation as a `LinearIsometryEquiv`

We also register the fact that `ℂ` is an `RCLike` field.

source
instance Complex.instModuleSelf :
Module ℂ ℂ

A shortcut instance to ensure computability; otherwise we get the noncomputable instance `Complex.instNormedField.toNormedModule.toModule`.

Equations

- Complex.instModuleSelf = Semiring.toModule

source
instance Complex.instNormedField :
NormedField ℂ
Equations

- One or more equations did not get rendered due to their size.

source
instance Complex.instDenselyNormedField :
DenselyNormedField ℂ
Equations

- Complex.instDenselyNormedField = { toNormedField := Complex.instNormedField, lt_norm_lt := Complex.instDenselyNormedField._proof_1 }

source
instance Complex.instNormedAlgebraOfReal {R : Type u_1} [NormedField R] [NormedAlgebra R ℝ] :
NormedAlgebra R ℂ
Equations

- Complex.instNormedAlgebraOfReal = { toAlgebra := Complex.instAlgebraOfReal, norm_smul_le := ⋯ }

source
@[instance 900]
instance NormedSpace.complexToReal {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] :
NormedSpace ℝ E

The module structure from `Module.complexToReal` is a normed space.

Equations

- NormedSpace.complexToReal = NormedSpace.restrictScalars ℝ ℂ E

source
@[instance 900]
instance NormedAlgebra.complexToReal {A : Type u_2} [SeminormedRing A] [NormedAlgebra ℂ A] :
NormedAlgebra ℝ A

The algebra structure from `Algebra.complexToReal` is a normed algebra.

Equations

- NormedAlgebra.complexToReal = NormedAlgebra.restrictScalars ℝ ℂ A

source
@[simp]
theorem Complex.nnnorm_intCast (n : ℤ) :
‖↑n‖₊ = ‖n‖₊
source
theorem Complex.continuous_normSq :
Continuous ⇑normSq
source
theorem Complex.nnnorm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :
‖ζ‖₊ = 1
source
theorem Complex.norm_eq_one_of_pow_eq_one {ζ : ℂ} {n : ℕ} (h : ζ ^ n = 1) (hn : n ≠ 0) :
‖ζ‖ = 1
source
theorem Complex.le_of_eq_sum_of_eq_sum_norm {ι : Type u_2} {a b : ℝ} (f : ι → ℂ) (s : Finset ι) (ha₀ : 0 ≤ a) (ha : ↑a = ∑ i ∈ s, f i) (hb : ↑b = ∑ i ∈ s, ↑‖f i‖) :
a ≤ b
source
theorem Complex.equivRealProd_apply_le (z : ℂ) :
‖equivRealProd z‖ ≤ ‖z‖
source
theorem Complex.equivRealProd_apply_le' (z : ℂ) :
‖equivRealProd z‖ ≤ 1 * ‖z‖
source
theorem Complex.lipschitz_equivRealProd :
LipschitzWith 1 ⇑equivRealProd
source
theorem Complex.antilipschitz_equivRealProd :
AntilipschitzWith (NNReal.sqrt 2) ⇑equivRealProd
source
theorem Complex.isUniformEmbedding_equivRealProd :
IsUniformEmbedding ⇑equivRealProd
source
instance Complex.instCompleteSpace :
CompleteSpace ℂ
source
instance Complex.instT2Space :
T2Space ℂ
source
def Complex.equivRealProdCLM :
ℂ ≃L[ℝ] ℝ × ℝ

The natural `ContinuousLinearEquiv` from `ℂ` to `ℝ × ℝ`.

Equations

- Complex.equivRealProdCLM = Complex.equivRealProdLm.toContinuousLinearEquivOfBounds 1 (√2) Complex.equivRealProd_apply_le' Complex.equivRealProdCLM._proof_2

Instances For

source
@[simp]
theorem Complex.equivRealProdCLM_symm_apply_im (a✝ : ℝ × ℝ) :
(equivRealProdCLM.symm a✝).im = a✝.2
source
@[simp]
theorem Complex.equivRealProdCLM_symm_apply_re (a✝ : ℝ × ℝ) :
(equivRealProdCLM.symm a✝).re = a✝.1
source
@[simp]
theorem Complex.equivRealProdCLM_apply (a✝ : ℂ) :
equivRealProdCLM a✝ = (a✝.re, a✝.im)
source
theorem Complex.equivRealProdCLM_symm_apply (p : ℝ × ℝ) :
equivRealProdCLM.symm p = ↑p.1 + ↑p.2 * I
source
instance Complex.instProperSpace :
ProperSpace ℂ
source
theorem Complex.tendsto_normSq_cocompact_atTop :
Filter.Tendsto (⇑normSq) (Filter.cocompact ℂ) Filter.atTop

The `normSq` function on `ℂ` is proper.

source
def Complex.reCLM :
ℂ →L[ℝ] ℝ

Continuous linear map version of the real part function, from `ℂ` to `ℝ`.

Equations

- Complex.reCLM = Complex.reLm.mkContinuous 1 Complex.reCLM._proof_1

Instances For

source
theorem Complex.continuous_re :
Continuous re
source
theorem Complex.uniformlyContinuous_re :
UniformContinuous re
source
@[simp]
theorem Complex.reCLM_coe :
↑reCLM = reLm
source
@[simp]
theorem Complex.reCLM_apply (z : ℂ) :
reCLM z = z.re
source
def Complex.imCLM :
ℂ →L[ℝ] ℝ

Continuous linear map version of the imaginary part function, from `ℂ` to `ℝ`.

Equations

- Complex.imCLM = Complex.imLm.mkContinuous 1 Complex.imCLM._proof_1

Instances For

source
theorem Complex.continuous_im :
Continuous im
source
theorem Complex.uniformlyContinuous_im :
UniformContinuous im
source
@[simp]
theorem Complex.imCLM_coe :
↑imCLM = imLm
source
@[simp]
theorem Complex.imCLM_apply (z : ℂ) :
imCLM z = z.im
source
theorem Complex.restrictScalars_one_smulRight' {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℂ E] (x : E) :
ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = reCLM.smulRight x + I • imCLM.smulRight x
source
theorem Complex.restrictScalars_one_smulRight (x : ℂ) :
ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 x) = x • 1
source
def Complex.conjLIE :
ℂ ≃ₗᵢ[ℝ] ℂ

The complex-conjugation function from `ℂ` to itself is an isometric linear equivalence.

Equations

- Complex.conjLIE = { toLinearEquiv := Complex.conjAe.toLinearEquiv, norm_map' := Complex.norm_conj }

Instances For

source
@[simp]
theorem Complex.conjLIE_apply (z : ℂ) :
conjLIE z = (starRingEnd ℂ) z
source
@[simp]
theorem Complex.conjLIE_symm :
conjLIE.symm = conjLIE
source
theorem Complex.isometry_conj :
Isometry ⇑(starRingEnd ℂ)
source
@[simp]
theorem Complex.dist_conj_conj (z w : ℂ) :
dist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = dist z w
source
@[simp]
theorem Complex.nndist_conj_conj (z w : ℂ) :
nndist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = nndist z w
source
theorem Complex.dist_conj_comm (z w : ℂ) :
dist ((starRingEnd ℂ) z) w = dist z ((starRingEnd ℂ) w)
source
theorem Complex.nndist_conj_comm (z w : ℂ) :
nndist ((starRingEnd ℂ) z) w = nndist z ((starRingEnd ℂ) w)
source
instance Complex.instContinuousStar :
ContinuousStar ℂ
source
theorem Complex.continuous_conj :
Continuous ⇑(starRingEnd ℂ)
source
theorem Complex.ringHom_eq_id_or_conj_of_continuous {f : ℂ →+* ℂ} (hf : Continuous ⇑f) :
f = RingHom.id ℂ ∨ f = starRingEnd ℂ

The only continuous ring homomorphisms from `ℂ` to `ℂ` are the identity and the complex conjugation.

source
def Complex.conjCLE :
ℂ ≃L[ℝ] ℂ

Continuous linear equiv version of the conj function, from `ℂ` to `ℂ`.

Equations

- Complex.conjCLE = { toLinearEquiv := Complex.conjLIE.toLinearEquiv, continuous_toFun := Complex.conjCLE._proof_1, continuous_invFun := Complex.conjCLE._proof_2 }

Instances For

source
@[simp]
theorem Complex.conjCLE_coe :
conjCLE.toLinearEquiv = conjAe.toLinearEquiv
source
@[simp]
theorem Complex.conjCLE_apply (z : ℂ) :
conjCLE z = (starRingEnd ℂ) z
source
def Complex.ofRealLI :
ℝ →ₗᵢ[ℝ] ℂ

Linear isometry version of the canonical embedding of `ℝ` in `ℂ`.

Equations

- Complex.ofRealLI = { toLinearMap := Complex.ofRealAm.toLinearMap, norm_map' := Complex.norm_real }

Instances For

source
@[simp]
theorem Complex.ofRealLI_apply (x : ℝ) :
ofRealLI x = ↑x
source
theorem Complex.isometry_ofReal :
Isometry ofReal
source
theorem Complex.continuous_ofReal :
Continuous ofReal
source
theorem Complex.isUniformEmbedding_ofReal :
IsUniformEmbedding ofReal
source
theorem RCLike.isUniformEmbedding_ofReal {𝕜 : Type u_2} [RCLike 𝕜] :
IsUniformEmbedding ofReal
source
theorem Filter.tendsto_ofReal_iff {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ} :
Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x) ↔ Tendsto f l (nhds x)
source
theorem Filter.tendsto_ofReal_iff' {α : Type u_2} {𝕜 : Type u_3} [RCLike 𝕜] {l : Filter α} {f : α → ℝ} {x : ℝ} :
Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x) ↔ Tendsto f l (nhds x)
source
theorem Filter.Tendsto.ofReal {α : Type u_2} {l : Filter α} {f : α → ℝ} {x : ℝ} (hf : Tendsto f l (nhds x)) :
Tendsto (fun (x : α) => ↑(f x)) l (nhds ↑x)
source
theorem Complex.ringHom_eq_ofReal_of_continuous {f : ℝ →+* ℂ} (h : Continuous ⇑f) :
f = ofRealHom

The only continuous ring homomorphism from `ℝ` to `ℂ` is the identity.

source
def Complex.ofRealCLM :
ℝ →L[ℝ] ℂ

Continuous linear map version of the canonical embedding of `ℝ` in `ℂ`.

Equations

- Complex.ofRealCLM = Complex.ofRealLI.toContinuousLinearMap

Instances For

source
@[simp]
theorem Complex.ofRealCLM_coe :
↑ofRealCLM = ofRealAm.toLinearMap
source
@[simp]
theorem Complex.ofRealCLM_apply (x : ℝ) :
ofRealCLM x = ↑x
source
noncomputable instance Complex.instRCLike :
RCLike ℂ
Equations

- One or more equations did not get rendered due to their size.

source
theorem RCLike.re_eq_complex_re :
⇑re = Complex.re
source
theorem RCLike.im_eq_complex_im :
⇑im = Complex.im
source
theorem RCLike.ofReal_eq_complex_ofReal :
ofReal = Complex.ofReal
source
theorem Complex.mul_conj' (z : ℂ) :
z * (starRingEnd ℂ) z = ↑‖z‖ ^ 2
source
theorem Complex.conj_mul' (z : ℂ) :
(starRingEnd ℂ) z * z = ↑‖z‖ ^ 2
source
theorem Complex.inv_eq_conj {z : ℂ} (hz : ‖z‖ = 1) :
z⁻¹ = (starRingEnd ℂ) z
source
theorem Complex.exists_norm_eq_mul_self (z : ℂ) :
∃ (c : ℂ), ‖c‖ = 1 ∧ ↑‖z‖ = c * z
source
theorem Complex.exists_norm_mul_eq_self (z : ℂ) :
∃ (c : ℂ), ‖c‖ = 1 ∧ c * ↑‖z‖ = z
source
theorem Complex.im_eq_zero_iff_isSelfAdjoint (x : ℂ) :
x.im = 0 ↔ IsSelfAdjoint x
source
theorem Complex.re_eq_ofReal_of_isSelfAdjoint {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) :
x.re = y ↔ x = ↑y
source
theorem Complex.ofReal_eq_re_of_isSelfAdjoint {x : ℂ} {y : ℝ} (hx : IsSelfAdjoint x) :
y = x.re ↔ ↑y = x
source
def RCLike.complexRingEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) :
𝕜 ≃+* ℂ

The natural isomorphism between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when `RCLike.im RCLike.I = 1`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem RCLike.complexRingEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (x : 𝕜) :
(complexRingEquiv h) x = ↑(re x) + ↑(im x) * Complex.I
source
@[simp]
theorem RCLike.complexRingEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (x : ℂ) :
(complexRingEquiv h).symm x = ↑x.re + ↑x.im * I
source
def RCLike.complexLinearIsometryEquiv {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) :
𝕜 ≃ₗᵢ[ℝ] ℂ

The natural `ℝ`-linear isometry equivalence between `𝕜` satisfying `RCLike 𝕜` and `ℂ` when `RCLike.im RCLike.I = 1`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem RCLike.complexLinearIsometryEquiv_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (a✝ : 𝕜) :
(complexLinearIsometryEquiv h) a✝ = (complexRingEquiv h).toFun a✝
source
@[simp]
theorem RCLike.complexLinearIsometryEquiv_symm_apply {𝕜 : Type u_2} [RCLike 𝕜] (h : im I = 1) (a✝ : ℂ) :
(complexLinearIsometryEquiv h).symm a✝ = (complexRingEquiv h).invFun a✝
source
theorem Complex.isometry_intCast :
Isometry Int.cast
source
theorem Complex.closedEmbedding_intCast :
Topology.IsClosedEmbedding Int.cast
source
theorem Complex.isClosed_range_intCast :
IsClosed (Set.range Int.cast)
source
theorem Complex.isOpen_compl_range_intCast :
IsOpen (Set.range Int.cast)ᶜ
source
theorem Complex.eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) :
z = ↑‖z‖
source
theorem Complex.orderClosedTopology :
OrderClosedTopology ℂ

We show that the partial order and the topology on `ℂ` are compatible. We turn this into an instance scoped to `ComplexOrder`.

source
theorem Complex.norm_of_nonneg' {x : ℂ} (hx : 0 ≤ x) :
↑‖x‖ = x
source
theorem Complex.re_nonneg_iff_nonneg {x : ℂ} (hx : IsSelfAdjoint x) :
0 ≤ x.re ↔ 0 ≤ x
source
theorem Complex.re_le_re {x y : ℂ} (h : x ≤ y) :
x.re ≤ y.re
source
@[simp]
theorem RCLike.re_to_complex {x : ℂ} :
re x = x.re
source
@[simp]
theorem RCLike.im_to_complex {x : ℂ} :
im x = x.im
source
@[simp]
theorem RCLike.I_to_complex :
I = Complex.I
source
@[simp]
theorem RCLike.normSq_to_complex {x : ℂ} :
normSq x = Complex.normSq x
source
@[simp]
theorem RCLike.hasSum_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} :
HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) x L ↔ HasSum f ((starRingEnd 𝕜) x) L
source
theorem RCLike.hasSum_conj' {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} :
HasSum (fun (x : α) => (starRingEnd 𝕜) (f x)) ((starRingEnd 𝕜) x) L ↔ HasSum f x L
source
@[simp]
theorem RCLike.summable_conj {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} :
Summable (fun (x : α) => (starRingEnd 𝕜) (f x)) L ↔ Summable f L
source
theorem RCLike.conj_tsum {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) :
(starRingEnd 𝕜) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd 𝕜) (f a)
source
@[simp]
theorem RCLike.hasSum_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ} {x : ℝ} :
HasSum (fun (x : α) => ↑(f x)) (↑x) L ↔ HasSum f x L
source
@[simp]
theorem RCLike.summable_ofReal {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → ℝ} :
Summable (fun (x : α) => ↑(f x)) L ↔ Summable f L
source
theorem RCLike.ofReal_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} (f : α → ℝ) :
↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
source
theorem RCLike.hasSum_re {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} (h : HasSum f x L) :
HasSum (fun (x : α) => re (f x)) (re x) L
source
theorem RCLike.hasSum_im {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜} (h : HasSum f x L) :
HasSum (fun (x : α) => im (f x)) (im x) L
source
theorem RCLike.re_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜} (h : Summable f L) :
re (∑'[L] (a : α), f a) = ∑'[L] (a : α), re (f a)
source
theorem RCLike.im_tsum {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {L : SummationFilter α} [L.NeBot] {f : α → 𝕜} (h : Summable f L) :
im (∑'[L] (a : α), f a) = ∑'[L] (a : α), im (f a)
source
theorem RCLike.hasSum_iff {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {L : SummationFilter α} (f : α → 𝕜) (c : 𝕜) :
HasSum f c L ↔ HasSum (fun (x : α) => re (f x)) (re c) L ∧ HasSum (fun (x : α) => im (f x)) (im c) L

We have to repeat the lemmas about `RCLike.re` and `RCLike.im` as they are not syntactic matches for `Complex.re` and `Complex.im`.

We do not have this problem with `ofReal` and `conj`, although we repeat them anyway for discoverability and to avoid the need to unify `𝕜`.

source
theorem Complex.hasSum_conj {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} :
HasSum (fun (x : α) => (starRingEnd ℂ) (f x)) x L ↔ HasSum f ((starRingEnd ℂ) x) L
source
theorem Complex.hasSum_conj' {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} :
HasSum (fun (x : α) => (starRingEnd ℂ) (f x)) ((starRingEnd ℂ) x) L ↔ HasSum f x L
source
theorem Complex.summable_conj {α : Type u_1} {f : α → ℂ} :
(Summable fun (x : α) => (starRingEnd ℂ) (f x)) ↔ Summable f
source
theorem Complex.conj_tsum {α : Type u_1} {L : SummationFilter α} (f : α → ℂ) :
(starRingEnd ℂ) (∑'[L] (a : α), f a) = ∑'[L] (a : α), (starRingEnd ℂ) (f a)
source
@[simp]
theorem Complex.hasSum_ofReal {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {x : ℝ} :
HasSum (fun (x : α) => ↑(f x)) (↑x) L ↔ HasSum f x L
source
@[simp]
theorem Complex.summable_ofReal {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} :
Summable (fun (x : α) => ↑(f x)) L ↔ Summable f L
source
theorem Complex.ofReal_tsum {α : Type u_1} {L : SummationFilter α} (f : α → ℝ) :
↑(∑'[L] (a : α), f a) = ∑'[L] (a : α), ↑(f a)
source
theorem Complex.hasSum_re {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} (h : HasSum f x L) :
HasSum (fun (x : α) => (f x).re) x.re L
source
theorem Complex.hasSum_im {α : Type u_1} {L : SummationFilter α} {f : α → ℂ} {x : ℂ} (h : HasSum f x L) :
HasSum (fun (x : α) => (f x).im) x.im L
source
theorem Complex.re_tsum {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ} (h : Summable f L) :
(∑'[L] (a : α), f a).re = ∑'[L] (a : α), (f a).re
source
theorem Complex.im_tsum {α : Type u_1} {L : SummationFilter α} [L.NeBot] {f : α → ℂ} (h : Summable f L) :
(∑'[L] (a : α), f a).im = ∑'[L] (a : α), (f a).im
source
theorem Complex.hasSum_iff {α : Type u_1} {L : SummationFilter α} (f : α → ℂ) (c : ℂ) :
HasSum f c L ↔ HasSum (fun (x : α) => (f x).re) c.re L ∧ HasSum (fun (x : α) => (f x).im) c.im L

### Define the "slit plane" `ℂ ∖ ℝ≤0` and provide some API #

source
def Complex.slitPlane :
Set ℂ

The slit plane is the complex plane with the closed negative real axis removed.

Equations

- Complex.slitPlane = {z : ℂ | 0 < z.re ∨ z.im ≠ 0}

Instances For

source
theorem Complex.mem_slitPlane_iff {z : ℂ} :
z ∈ slitPlane ↔ 0 < z.re ∨ z.im ≠ 0
source
theorem Complex.mem_slitPlane_or_neg_mem_slitPlane {z : ℂ} (hz : z ≠ 0) :
z ∈ slitPlane ∨ -z ∈ slitPlane
source
theorem Complex.slitPlane_eq_union :
slitPlane = {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0}
source
theorem Complex.isOpen_slitPlane :
IsOpen slitPlane
source
@[simp]
theorem Complex.ofReal_mem_slitPlane {x : ℝ} :
↑x ∈ slitPlane ↔ 0 < x
source
@[simp]
theorem Complex.neg_ofReal_mem_slitPlane {x : ℝ} :
-↑x ∈ slitPlane ↔ x < 0
source
@[simp]
theorem Complex.one_mem_slitPlane :
1 ∈ slitPlane
source
@[simp]
theorem Complex.zero_notMem_slitPlane :
0 ∉ slitPlane
source
@[deprecated Complex.zero_notMem_slitPlane (since := "2025-05-23")]
theorem Complex.zero_not_mem_slitPlane :
0 ∉ slitPlane

Alias of `Complex.zero_notMem_slitPlane`.

source
@[simp]
theorem Complex.natCast_mem_slitPlane {n : ℕ} :
↑n ∈ slitPlane ↔ n ≠ 0
source
@[simp]
theorem Complex.ofNat_mem_slitPlane (n : ℕ) [n.AtLeastTwo] :
OfNat.ofNat n ∈ slitPlane
source
theorem Complex.mem_slitPlane_iff_not_le_zero {z : ℂ} :
z ∈ slitPlane ↔ ¬z ≤ 0
source
theorem Complex.compl_Iic_zero :
(Set.Iic 0)ᶜ = slitPlane
source
theorem Complex.slitPlane_ne_zero {z : ℂ} (hz : z ∈ slitPlane) :
z ≠ 0
source
theorem Complex.ball_one_subset_slitPlane :
Metric.ball 1 1 ⊆ slitPlane

The slit plane includes the open unit ball of radius `1` around `1`.

source
theorem Complex.mem_slitPlane_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) :
1 + z ∈ slitPlane

The slit plane includes the open unit ball of radius `1` around `1`.

source
theorem Complex.subset_slitPlane_iff_of_subset_sphere {r : ℝ} {s : Set ℂ} (hs : s ⊆ Metric.sphere 0 r) :
s ⊆ slitPlane ↔ -↑r ∉ s

A subset of the circle centered at the origin in `ℂ` of radius `r` is a subset of the `slitPlane` if it does not contain `-r`.

source
theorem IsCompact.reProdIm {s t : Set ℝ} (hs : IsCompact s) (ht : IsCompact t) :
IsCompact (s ×ℂ t)
source
theorem realPart.norm_le {A : Type u_1} [SeminormedAddCommGroup A] [StarAddMonoid A] [NormedSpace ℂ A] [StarModule ℂ A] [NormedStarGroup A] (x : A) :
‖realPart x‖ ≤ ‖x‖
source
theorem imaginaryPart.norm_le {A : Type u_1} [SeminormedAddCommGroup A] [StarAddMonoid A] [NormedSpace ℂ A] [StarModule ℂ A] [NormedStarGroup A] (x : A) :
‖imaginaryPart x‖ ≤ ‖x‖