inner_add_right — Mathlib

English

The inner product is linear in the second argument: ⟪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_add_right (x y z : E) : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ :=
  by
  rw [← inner_conj_symm, inner_add_left, RingHom.map_add]
  simp only [inner_conj_symm]

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