prod_Icc_cast — Mathlib

English

Let h be an equality n = m. For f: Fin m → M and a,b ∈ Fin n, the product over Icc(cast h a, cast h b) equals the product over Icc(a,b) with i cast h inside.

Русский

Пусть h: n=m. Для f: Fin m → M и a,b ∈ Fin n произведение по Icc(cast h a, cast h b) равно произведению по Icc(a,b) с заменой индексов на i cast h.

LaTeX

$$$\displaystyle \prod_{i \in \mathrm{Icc}(\mathrm{cast}(h,a),\mathrm{cast}(h,b))} f(i) = \prod_{i \in \mathrm{Icc}(a,b)} f(i \mathrm{ cast } h).$$$

Lean4

@[to_additive]
theorem prod_Icc_cast (h : n = m) (f : Fin m → M) (a b : Fin n) :
    ∏ i ∈ Icc (a.cast h) (b.cast h), f i = ∏ i ∈ Icc a b, f (i.cast h) := by simp [← map_finCongr_Icc]

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