inner_neg_right — Mathlib

English

For all x, y in E, the inner product is linear in the second argument; in particular ⟨x, -y⟩ = -⟨x, y⟩.

Русский

Для любых x, y в E скалярное (A-)вложенное произведение линейно по второму аргументу; в частности ⟨x, -y⟩ = -⟨x, y⟩.

LaTeX

$$$\\\\langle x, -y \\\\rangle_A = -\\\\langle x, y \\\\rangle_A$$$

Lean4

@[simp]
theorem inner_neg_right {x y : E} : ⟪x, -y⟫ = -⟪x, y⟫ := by simp [← innerₛₗ_apply]

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