inner_zero_right

Mathlib.Analysis.InnerProductSpace.Basic

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

English

The real part is symmetric under swap: 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

@[simp]
theorem inner_zero_right (x : E) : ⟪x, 0⟫ = 0 := by rw [← inner_conj_symm, inner_zero_left, RingHom.map_zero]

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

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

Разделы

Аффилиация

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