prod_Iio_castAdd — Mathlib

English

Let M be a commutative monoid. For n ∈ ℕ, m ∈ ℕ, f : Fin (n + m) → M, a ∈ Fin n, the product over i < a.castAdd m equals the product over i < a of f(i.castAdd m).

Русский

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

LaTeX

$$$$ \\displaystyle \\prod_{i < a^{\\mathrm{castAdd} m}} f(i) = \\prod_{i < a} f(i^{\\mathrm{castAdd} m}) $$$$

Lean4

@[to_additive]
theorem prod_Iio_castAdd (m : ℕ) (f : Fin (n + m) → M) (a : Fin n) :
    ∏ i < a.castAdd m, f i = ∏ i < a, f (i.castAdd m) := by simp [← map_castAddEmb_Iio]

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