imLm — Mathlib

English

imLm is the imaginary-part linear map; it preserves addition and scalar multiplication by real numbers.

Русский

imLm — линейное отображение мнимой части, сохраняющее сложение и умножение на вещественные числа.

LaTeX

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

Lean4

/-- The imaginary part in an `RCLike` field, as a linear map. -/
def imLm : K →ₗ[ℝ] ℝ :=
  { im with map_smul' := smul_im }

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