conj_wInner_symm — Mathlib

English

Weighted inner product is linear in the first argument: ⟪-f, g⟫_[𝕜, w] = −⟪f, g⟫_[𝕜, w].

Русский

Взвешенное скалярное произведение линейно по первому аргументу: ⟪-f, g⟫ = −⟪f, g⟫.

LaTeX

$$$ \\langle -f, g \\rangle_{𝕜,[w]} = -\\langle f, g \\rangle_{𝕜,[w]} $$$

Lean4

@[simp]
theorem conj_wInner_symm (w : ι → ℝ) (f g : ∀ i, E i) : conj ⟪f, g⟫_[𝕜, w] = ⟪g, f⟫_[𝕜, w] := by
  simp [wInner, map_sum, inner_conj_symm, rclike_simps]

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