tprod_eq_zero_mul' — Mathlib

English

For a function f: ℕ → M with M a monoid and Multipliable f, the infinite product ∏' i, f i equals f(0) times the tail product ∏' i, f(i+1).

Русский

Для функции f: ℕ → M с моноидной структурой и условием Multipliable f бесконечное произведение ∏' i, f i равно f(0) умножить на хвостовое произведение ∏' i, f(i+1).

LaTeX

$$$\prod' b, f b = f 0 \cdot \prod' b, f (b+1)$$$

Lean4

@[to_additive]
theorem tprod_eq_zero_mul' {f : ℕ → M} (hf : Multipliable (fun n ↦ f (n + 1))) : ∏' b, f b = f 0 * ∏' b, f (b + 1) := by
  simpa only [prod_range_one] using hf.prod_mul_tprod_nat_mul'.symm

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