inner_sub_right

Mathlib.Analysis.InnerProductSpace.Defs

URI: https://scilib.ai/kg/mathlib#InnerProductSpace.Core.inner_sub_right

English

⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫.

Русский

⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫.

LaTeX

$$$\\\\langle x, y - z \\\\rangle = \\\\langle x, y \\\\rangle - \\\\langle x, z \\\\rangle$$$

Lean4

theorem inner_sub_right (x y z : F) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ := by
  simp [sub_eq_add_neg, inner_add_right, inner_neg_right]

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

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

Разделы

Аффилиация

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