conjCLE_norm

Mathlib.Analysis.Complex.OperatorNorm

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

English

The norm of conjCLE, the complex conjugation as a linear map over R, is 1.

Русский

Норма conjCLE, комплексного сопряжения как линейного отображения над R, равна 1.

LaTeX

$$$\\|\\mathrm{conjCLE}\\| = 1$$$

Lean4

@[simp]
theorem conjCLE_norm : ‖(conjCLE : ℂ →L[ℝ] ℂ)‖ = 1 :=
  conjLIE.toLinearIsometry.norm_toContinuousLinearMap

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

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

Разделы

Аффилиация

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