prod_Iio_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_Iio_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_Iio]

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