enorm_conj

Mathlib.Analysis.RCLike.Basic

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

English

Conjugation preserves the ENorm: enorm(conj z) = enorm(z).

Русский

Сопряжение сохраняет ENorm: enorm(conj z) = enorm z.

LaTeX

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

Lean4

@[simp 1100, rclike_simps]
theorem enorm_conj (z : K) : ‖conj z‖ₑ = ‖z‖ₑ := by simp [enorm]

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

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

Разделы

Аффилиация

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