inner_single_right — Mathlib

English

The inner product of a vector v with the i-th basis vector equals a times conj(v_i).

Русский

Скалярное произведение вектора v на i-й базисный вектор равно a · conj(v_i).

LaTeX

$$$\langle v, \mathrm{single}_i(a)\rangle = a\, \overline{v_i}$$$

Lean4

theorem inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
    ⟪v, EuclideanSpace.single i (a : 𝕜)⟫ = a * conj (v i) := by simp [PiLp.inner_apply]

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