reCLM — Mathlib

English

imLm is the imaginary-part real-linear map, from K to ℝ, with smul compatibility.

Русский

imLm — линейное по отношению к ℝ отображение мнимой части от K в ℝ, с совместимостью smul.

LaTeX

$$$\text{imLm}: K \to_{\mathbb{R}} \mathbb{R} \text{ is linear}$$$

Lean4

/-- The real part in an `RCLike` field, as a continuous linear map. -/
noncomputable def reCLM : StrongDual ℝ K :=
  reLm.mkContinuous 1 fun x => by
    rw [one_mul]
    exact abs_re_le_norm x

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