dist_conj_self — Mathlib

English

For any z = a + bi, the distance between z and its conjugate is dist(z, \overline{z}) = 2|b|.

Русский

Для z = a + bi расстояние до сопряжённого равно dist(z, \overline{z}) = 2|b|.

LaTeX

$$$\\\\operatorname{dist}(z, \\overline{z}) = 2 \\lvert \\operatorname{Im} z \\rvert$$$

Lean4

theorem dist_conj_self (z : ℂ) : dist (conj z) z = 2 * |z.im| := by
  rw [dist_of_re_eq (conj_re z), conj_im, dist_comm, Real.dist_eq, sub_neg_eq_add, ← two_mul, _root_.abs_mul,
    abs_of_pos (zero_lt_two' ℝ)]

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