wInner_smul_left — Mathlib

English

For a scalar c in 𝕝 acting on the left, the weighted inner product satisfies ⟪c • f, g⟫ = overline(c) • ⟪f, g⟫.

Русский

Для скаляра c слева выполняется ⟪c • f, g⟫ = conj(c) • ⟪f, g⟫.

LaTeX

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

Lean4

theorem wInner_smul_left {𝕝 : Type*} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [StarModule 𝕝 𝕜] [SMulCommClass ℝ 𝕝 𝕜]
    [∀ i, Module 𝕝 (E i)] [∀ i, IsScalarTower 𝕝 𝕜 (E i)] (c : 𝕝) (w : ι → ℝ) (f g : ∀ i, E i) :
    ⟪c • f, g⟫_[𝕜, w] = star c • ⟪f, g⟫_[𝕜, w] := by
  simp_rw [wInner, Pi.smul_apply, inner_smul_left_eq_star_smul, starRingEnd_apply, smul_sum, smul_comm (w _)]

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