English
If f is Multipliable, then the finite-prefix times shifted tail identity yields the full product: ((∏_{i<k} f(i)) · ∏' i, f(i+k)) = ∏' i, f(i)).
Русский
Если f мультиплируема, то произведение первых k членов умноженное на хвостовое сдвинутое произведение равно полному произведению.
LaTeX
$$$\left(\prod_{i=0}^{k-1} f(i)\right) \cdot \prod' i, f(i+k) = \prod' i, f(i)$$$
Lean4
@[to_additive HasSum.nat_add_neg_add_one]
theorem nat_mul_neg_add_one {f : ℤ → M} (hf : HasProd f m) : HasProd (fun n : ℕ ↦ f n * f (-(n + 1))) m :=
by
change HasProd (fun n : ℕ ↦ f n * f (Int.negSucc n)) m
have : Injective Int.negSucc := @Int.negSucc.inj
refine hf.hasProd_of_prod_eq fun u ↦ ?_
refine
⟨u.preimage _ Nat.cast_injective.injOn ∪ u.preimage _ this.injOn, fun v' hv' ↦
⟨v'.image Nat.cast ∪ v'.image Int.negSucc, fun x hx ↦ ?_, ?_⟩⟩
· simp only [mem_union, mem_image]
cases x
· exact Or.inl ⟨_, hv' (by simpa using Or.inl hx), rfl⟩
· exact Or.inr ⟨_, hv' (by simpa using Or.inr hx), rfl⟩
· rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn, prod_mul_distrib]
simp only [disjoint_iff_ne, mem_image, ne_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
not_false_eq_true, implies_true, reduceCtorEq]
