prod_Iio_castLE — Mathlib

English

Let M be a commutative monoid. For h : n ≤ m, f : Fin m → M, a : Fin n, the product over i ∈ Iio (a.castLE h) equals the product over i ∈ Iio a of f(i.castLE h).

Русский

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

LaTeX

$$$$ \\displaystyle \\prod_{i \\in \\mathrm{Iio}(a^{\\mathrm{castLE} h})} f(i) = \\prod_{i \\in \\mathrm{Iio} a} f(i^{\\mathrm{castLE} h}) $$$$

Lean4

@[to_additive]
theorem prod_Iio_castLE (h : n ≤ m) (f : Fin m → M) (a : Fin n) : ∏ i < a.castLE h, f i = ∏ i < a, f (i.castLE h) := by
  simp [← map_castLEEmb_Iio]

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