complexOfReal — Mathlib

English

The complex extension of a real-linear map agrees with the original map as a function.

Русский

Расширение до комплексных скалярных относится к исходной карте как к функции.

LaTeX

$$$\ell.complexOfReal(h) = (\ell : \mathbb{C} \to E)$$$

Lean4

/-- Construct a complex-linear map from a real-linear map `ℓ` that maps `I` to `I • ℓ 1`.
-/
def complexOfReal (ℓ : ℂ →ₗ[ℝ] E) (h : ℓ I = I • ℓ 1) : ℂ →ₗ[ℂ] E
    where
  __ := ℓ
  map_smul' := real_linearMap_map_smul_complex h

Похожие утверждения