real_inner_smul_right

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#real_inner_smul_right

English

The real part is symmetric with swapped arguments: Re⟪x,y⟫ = Re⟪y,x⟫.

Русский

Действительная часть симметрична: Re⟪x,y⟫ = Re⟪y,x⟫.

LaTeX

$$$\operatorname{Re}\langle x, y\rangle = \operatorname{Re}\langle y, x\rangle$$$

Lean4

theorem real_inner_smul_right (x y : F) (r : ℝ) : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ :=
  inner_smul_right _ _ _

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

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

Разделы

Аффилиация

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