prod_inv_index — Mathlib

English

For a finite index set ι and a function f, the product over the inverse indices equals the product over the original indices of the inverses: ∏ i∈s⁻¹ f(i) = ∏ i∈s f(i)⁻¹.

Русский

Для конечного множества индексов ι и функции f верно: ∏_{i∈s⁻¹} f(i) = ∏_{i∈s} f(i)⁻¹.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem prod_inv_index [InvolutiveInv ι] (s : Finset ι) (f : ι → α) : ∏ i ∈ s⁻¹, f i = ∏ i ∈ s, f i⁻¹ :=
  prod_image inv_injective.injOn

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