prod_Iic_castSucc — Mathlib

English

Let M be a commutative monoid. For f : Fin (n + 1) → M and a : Fin n, the product over i ∈ Iic (a.castSucc) equals the product over i ∈ Iic a of f i.castSucc.

Русский

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

LaTeX

$$$$ \\displaystyle \\prod_{i \\in \\mathrm{Iic}(a^{\\mathrm{castSucc}})} f(i) = \\prod_{i \\in \\mathrm{Iic} a} f(i^{\\mathrm{castSucc}}) $$$$

Lean4

@[to_additive]
theorem prod_Iic_castSucc (f : Fin (n + 1) → M) (a : Fin n) : ∏ i ≤ a.castSucc, f i = ∏ i ≤ a, f i.castSucc := by
  simp [← map_castSuccEmb_Iic]

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