im_balance — Mathlib

English

For a finite index set, balance f a is a complex number; its imaginary part equals the balance of the imaginary parts: Im(balance f a) = balance (Im ∘ f) a.

Русский

Для конечного набора индексов значение balance f a — комплексное число; его мнимая часть равна балансу мнимых частей: Im(balance f a) = balance (Im ∘ f) a.

LaTeX

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

Lean4

@[simp]
theorem im_balance [Fintype α] (f : α → ℂ) (a : α) : im (balance f a) = balance (im ∘ f) a := by simp [balance]

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