conj_ofReal

Mathlib.Analysis.RCLike.Basic

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

← MathLib Explorer

English

Conjugation fixes real numbers: conj(ofReal r) = ofReal r.

Русский

Сопряжение фиксирует вещественные числа: conj(ofReal r) = ofReal r.

LaTeX

$$$\operatorname{conj}(\operatorname{ofReal}(r)) = \operatorname{ofReal}(r)$$$

Lean4

@[simp, rclike_simps]
theorem conj_ofReal (r : ℝ) : conj (r : K) = (r : K) :=
  by
  rw [ext_iff]
  simp only [ofReal_im, conj_im, conj_re, and_self_iff, neg_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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