imLm — Mathlib

English

The imaginary part function Im: ℂ → ℝ is ℝ-linear.

Русский

Функция мнимой части Im: ℂ → ℝ является вещественно-линейной.

LaTeX

$$$ \mathrm{imLm} : \mathbb{C} \to_{\mathbb{R}} \mathbb{R} \text{ is } \mathbb{R}\text{-linear}. $$$

Lean4

/-- Linear map version of the imaginary part function, from `ℂ` to `ℝ`. -/
def imLm : ℂ →ₗ[ℝ] ℝ where
  toFun x := x.im
  map_add' := add_im
  map_smul' := by simp

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