ofReal_sub — Mathlib

English

For real numbers r and s, embedding them into complex numbers preserves subtraction: the complex embedding of r − s equals the difference of the embeddings.

Русский

Для вещественных чисел r и s вложение их в комплексные числа сохраняет вычитание: отображение r − s в ℝC равно разности отображений r и s.

LaTeX

$$$$\\operatorname{ofReal}(r - s) = \\operatorname{ofReal}(r) - \\operatorname{ofReal}(s).$$$$

Lean4

@[simp, norm_cast]
theorem ofReal_sub (r s : ℝ) : ((r - s : ℝ) : ℂ) = r - s :=
  Complex.ext_iff.2 <| by simp [ofReal]

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