inner_sub_left

Mathlib.Analysis.InnerProductSpace.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inner_sub_left (x y z : F) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ := by
  simp [sub_eq_add_neg, inner_add_left, inner_neg_left]

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

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

Разделы

Аффилиация

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