prod_congr' — Mathlib

English

If a = b, then reindexing the product by cast(i) yields the same product: the product over Fin a of f(i.cast h) equals the product over Fin b of f(i).

Русский

Если a = b, то перенумерация индексов через cast h сохраняет произведение: сумма по Fin a f(i.cast h) равна произведению по Fin b f i.

LaTeX

$$$\displaystyle \prod_{i : \mathrm{Fin}(a)} f(i\!\text{ cast } h) = \prod_{i : \mathrm{Fin}(b)} f(i).$$$

Lean4

@[to_additive]
theorem prod_congr' {a b : ℕ} (f : Fin b → M) (h : a = b) : (∏ i : Fin a, f (i.cast h)) = ∏ i : Fin b, f i :=
  by
  subst h
  congr

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