prod_Iic_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 \\le a^{\\mathrm{cast}(h)}} f(i) = \\prod_{i \\le a} f(i^{\\mathrm{cast}(h)}) $$$$

Lean4

@[to_additive]
theorem prod_Iic_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_Iic]

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