div_re_ofReal

Mathlib.Analysis.RCLike.Basic

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

English

For z ∈ K and real r, the real part of z/r equals Re(z)/r.

Русский

Для z ∈ K и вещественного r, Re(z/r) = Re(z)/r.

LaTeX

$$$$ \operatorname{Re}\left(\frac{z}{r}\right) = \frac{\operatorname{Re}(z)}{r}. $$$$

Lean4

theorem div_re_ofReal {z : K} {r : ℝ} : re (z / r) = re z / r := by
  rw [div_eq_inv_mul, div_eq_inv_mul, ← ofReal_inv, re_ofReal_mul]

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

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

Разделы

Аффилиация

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