English
For multipliable f,g: ℕ→M, the product over ℤ of Int.rec f g equals the product over ℕ of f times the product over ℕ of g.
Русский
Для мультиплируемых f,g: ℕ→M, произведение по ℤ Int.rec f g равно произведению по ℕ f умноженному на произведение по ℕ g.
LaTeX
$$$\prod'_{n:\mathbb{Z}} \text{Int.rec}(f,g)(n) = (\prod'_{n:\mathbb{N}} f(n)) \cdot (\prod'_{n:\mathbb{N}} g(n))$$$
Lean4
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both multipliable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position). -/
@[to_additive /-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` are both summable then so is the
`ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position). -/
]
theorem int_rec {f g : ℕ → M} (hf : Multipliable f) (hg : Multipliable g) : Multipliable (Int.rec f g) :=
.of_nat_of_neg_add_one hf hg
