prod_Ici_cast — Mathlib

English

Let M be a commutative monoid. For h : n = m, a ∈ Fin n, and f : Fin m → M, the product over all i with i ≥ a.cast h equals the product over i ≥ a of f(i.cast h).

Русский

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

LaTeX

$$$$ \\displaystyle \\prod_{i \\ge a^{\\mathrm{cast}(h)}} f(i) = \\prod_{i \\ge a} f(i^{\\mathrm{cast}(h)}) $$$$

Lean4

@[to_additive]
theorem prod_Ici_cast (h : n = m) (f : Fin m → M) (a : Fin n) : ∏ i ≥ a.cast h, f i = ∏ i ≥ a, f (i.cast h) := by
  simp [← map_finCongr_Ici]

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