reLm — Mathlib

English

There exists a real-linear map from the complex numbers to the real numbers given by taking the real part. This map is linear over R and sends a+bi to a.

Русский

Существует действительное линейное отображение от комплексных чисел к действительным, задаваемое взятием вещественной части: (a+bi) ↦ a.

LaTeX

$$$ \\mathrm{re\\_lm}: \\mathbb{C} \\to_{\\mathbb{R}} \\mathbb{R},\\qquad \\mathrm{re\\_lm}(a+bi)=a $$$

Lean4

/-- Linear map version of the real part function, from `ℂ` to `ℝ`. -/
def reLm : ℂ →ₗ[ℝ] ℝ where
  toFun x := x.re
  map_add' := add_re
  map_smul' := by simp

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