inner

Mathlib.Analysis.InnerProductSpace.Basic

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

English

For w,z ∈ ℂ, the real inner product on ℂ satisfies ⟪w,z⟫_ℝ = (z·conj w).re.

Русский

Для комплексных чисел w,z ∈ ℂ вещественное внутреннее произведение удовлетворяет ⟪w,z⟫_ℝ = (z·conj w).ре.

LaTeX

$$$\\langle w,z\\rangle_{\\mathbb{R}} = \\operatorname{Re}(z\\overline{w}).$$$

Lean4

@[simp]
protected theorem inner (w z : ℂ) : ⟪w, z⟫_ℝ = (z * conj w).re :=
  rfl

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

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

Разделы

Аффилиация

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