re_comp_balance — Mathlib

English

The real part commutes with balance under real embedding: Re balance f = balance (Re ∘ f).

Русский

Действительная часть коммутирует с балансом при вложении в комплекс: Re balance f = balance (Re ∘ f).

LaTeX

$$$$ \operatorname{Re} \circ \operatorname{balance} f = \operatorname{balance} (\operatorname{Re} \circ f) $$$$

Lean4

@[simp]
theorem re_comp_balance {ι : Type*} [Fintype ι] (f : ι → ℂ) : re ∘ balance f = balance (re ∘ f) :=
  funext <| re_balance _

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