inner_add_right — Mathlib

English

Let x, y, z be elements of an inner product space. Then ⟪x, y+z⟫ = ⟪x, y⟫ + ⟪x, z⟫.

Русский

Пусть x, y, 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 : F) : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ := by
  rw [← inner_conj_symm, inner_add_left, RingHom.map_add]; simp only [inner_conj_symm]

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