wInner_const_left — Mathlib

English

A scalar c acting on the left yields a conjugate-scaled inner product: ⟪c • f, g⟫ = star(c) • ⟪f, g⟫.

Русский

Скаляр слева действует через сопряжение: ⟪c • f, g⟫ = conj(c) • ⟪f, g⟫.

LaTeX

$$$⟪c \cdot f, g\rangle_{𝕂, w} = \overline{c} \;⟪f, g⟫_{𝕂, w}$$$

Lean4

theorem wInner_const_left (a : 𝕜) (f : ι → 𝕜) : ⟪const _ a, f⟫_[𝕜, w] = (∑ i, w i • f i) * conj a := by
  simp [wInner, const_apply, sum_mul]

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