dist_conj_conj

Mathlib.Analysis.Complex.Basic

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

English

dist(conj z, conj w) = dist(z, w).

Русский

dist(сопряжение z, сопряжение w) = dist(z, w).

LaTeX

$$$$ \\operatorname{dist}(\\overline{z}, \\overline{w}) = \\operatorname{dist}(z,w). $$$$

Lean4

@[simp]
theorem dist_conj_conj (z w : ℂ) : dist (conj z) (conj w) = dist z w :=
  isometry_conj.dist_eq z w

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

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

Разделы

Аффилиация

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