nndist_conj_conj

Mathlib.Analysis.Complex.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem nndist_conj_conj (z w : ℂ) : nndist (conj z) (conj w) = nndist z w :=
  isometry_conj.nndist_eq z w

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

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

Разделы

Аффилиация

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