conj_tsum — Mathlib

English

Let α be an index set and 𝕜 a field with an involution. For any f: α → 𝕜, the complex conjugate of the (L-weighted) sum equals the sum of the conjugates: conj( ∑'[L] a, f(a) ) = ∑'[L] a, conj(f(a)).

Русский

Пусть α — множество индексов, 𝕜 — поле с инволюцией. Для любой функции f : α → 𝕜 выполнено: сопряжение суммы равно сумме сопряжённых: conj( ∑'[L] a, f(a) ) = ∑'[L] a, conj(f(a)).

LaTeX

$$$ \\overline{\\sum'[L] a, f(a)} = \\sum'[L] a, \\overline{f(a)} $$$

Lean4

theorem conj_tsum (f : α → 𝕜) : conj (∑'[L] a, f a) = ∑'[L] a, conj (f a) :=
  tsum_star

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