nnnorm_conj

Mathlib.Analysis.RCLike.Basic

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

English

The nonnegative norm is preserved under conjugation: nnnorm(conj z) = nnnorm(z).

Русский

Нормa без знака сохраняется при сопряжении: nnnorm(conj z) = nnnorm(z).

LaTeX

$$$$ \|\overline{z}\|_{nn} = \|z\|_{nn}. $$$$

Lean4

@[simp 1100, rclike_simps]
theorem nnnorm_conj (z : K) : ‖conj z‖₊ = ‖z‖₊ := by simp [nnnorm]

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

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

Разделы

Аффилиация

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