Theorems · Definition · complex analysis

ContinuousLinearMap.complexOfReal

{E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] → (ℓ : ℂ →L[ℝ] E) → ℓ Complex.I = Complex.I • ℓ 1 → ℂ →L[ℂ] E

Construct a continuous complex-linear map from a continuous real-linear map ℓ that maps I to I • ℓ 1.

Defined in

Mathlib.Analysis.Complex.Conformal

Cited by

10 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace