sum_inv_index — Mathlib

English

For a finite index set and additive group, the sum over the inverse indices equals the sum over the original indices of the inverses: ∑ i∈s⁻¹ f(i) = ∑ i∈s f(i)⁻¹.

Русский

Для конечного множества индексов и аддитивной группы: сумма по обратным индексам равна сумме по исходным индексам взятой обратной величиной.

LaTeX

$$$\sum_{i \in s^{-1}} f(i) = \sum_{i \in s} f(i)^{-1}$$$

Lean4

@[to_additive existing, simp]
theorem sum_inv_index [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∑ i ∈ s⁻¹, f i = ∑ i ∈ s, f i⁻¹ :=
  sum_image inv_injective.injOn

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