prod_Ioc_cast — Mathlib

English

Let h : n = m and f : Fin m → M. The product over Ioc(cast h a)(cast h b) equals the product over Ioc a b with indices cast by h.

Русский

Пусть h: n=m и f: Fin m → M. Произведение по Ioc(cast h a)(cast h b) равно произведению по Ioc a b с индексами, приведёнными через h.

LaTeX

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

Lean4

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

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