inner_sub_left — Mathlib

English

The inner product distributes over subtraction in the first argument: ⟪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 : E) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ := by simp [sub_eq_add_neg, inner_add_left]

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