inner_add_left — Mathlib

English

For any x, y, z in F, the inner product is linear in the first argument: ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫.

Русский

Для любых x, y, z в F, скалярное произведение линейно по первому аргументу: ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫.

LaTeX

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

Lean4

theorem inner_add_left (x y z : F) : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=
  c.add_left _ _ _

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