inner_re_zero_left

Mathlib.Analysis.InnerProductSpace.Basic

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

English

The inner product with zero on the right is zero: ⟪x, 0⟫ = 0.

Русский

Скалярное произведение с нулём справа равно нулю: ⟪x, 0⟫ = 0.

LaTeX

$$$\langle x, 0\rangle = 0$$$

Lean4

theorem inner_re_zero_left (x : E) : re ⟪0, x⟫ = 0 := by simp only [inner_zero_left, AddMonoidHom.map_zero]

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

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

Разделы

Аффилиация

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