wInner_smul_right — Mathlib

English

For a scalar c acting on the right, ⟪f, c • g⟫ = c • ⟪f, g⟫.

Русский

Для скаляра c справа: ⟪f, c • g⟫ = c • ⟪f, g⟫.

LaTeX

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

Lean4

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

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