im_comp_balance — Mathlib

English

The imaginary part commutes with balance under imaginary embedding: Im ∘ balance f = balance (Im ∘ f).

Русский

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

LaTeX

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

Lean4

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

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