ofReal_add — Mathlib

English

For real numbers r, s, embedding into the complex plane preserves addition: ((r + s) : ℂ) = r + s.

Русский

Для действительных чисел r, s вложение в комплекс сохраняет сложение: ((r + s) : ℂ) = r + s.

LaTeX

$$$((r+s) : \mathbb{C}) = r + s$$$

Lean4

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

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