sum_inner

Mathlib.Analysis.InnerProductSpace.Basic

URI: https://scilib.ai/kg/mathlib#sum_inner

← MathLib Explorer

English

For r in a star-ring, ⟪r x, y⟫ = r† ⟪x, y⟫.

Русский

Для r в звёздочном кольце, ⟪r x, y⟫ = r† ⟪x, y⟫.

LaTeX

$$$\langle r x, y\rangle = r^{\dagger} \langle x, y\rangle$$$

Lean4

/-- An inner product with a sum on the left. -/
theorem sum_inner {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) : ⟪∑ i ∈ s, f i, x⟫ = ∑ i ∈ s, ⟪f i, x⟫ :=
  map_sum (sesqFormOfInner (𝕜 := 𝕜) (E := E) x) _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru