English
If HasProd f m and HasProd g m' then HasProd (Int.rec f g) (m m').
Русский
Если HasProd f и HasProd g заданы, то HasProd Int.rec f g имеет произведение m·m'.
LaTeX
$$$\text{HasProd}(\text{Int.rec } f g) = m \cdot m'$$$
Lean4
/-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have products `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
product `a + b`. -/
@[to_additive /-- If `f₀, f₁, f₂, ...` and `g₀, g₁, g₂, ...` have sums `a`, `b` respectively, then
the `ℤ`-indexed sequence: `..., g₂, g₁, g₀, f₀, f₁, f₂, ...` (with `f₀` at the `0`-th position) has
sum `a + b`. -/
]
theorem int_rec {f g : ℕ → M} (hf : HasProd f m) (hg : HasProd g m') : HasProd (Int.rec f g) (m * m') :=
HasProd.of_nat_of_neg_add_one hf hg
