conj_ofReal

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.conj_ofReal

English

Conjugation fixes real numbers: conj(r) = r for every real r.

Русский

Сопряжение фиксирует действительные числа: conj(r) = r для всех r ∈ ℝ.

LaTeX

$$$\overline{r} = r\quad (r \in \mathbb{R})$$$

Lean4

@[simp]
theorem conj_ofReal (r : ℝ) : conj (r : ℂ) = r :=
  Complex.ext_iff.2 <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru