prod_Ioi_cast — Mathlib

English

Let M be a commutative monoid. For h : n = m, a ∈ Fin n, and f : Fin m → M, the product over 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 > a^{\\mathrm{cast}(h)}} f(i) = \\prod_{i > a} f(i^{\\mathrm{cast}(h)}) $$$$

Lean4

@[to_additive]
theorem prod_Ioi_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_Ioi]

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