Theorems · Theorem · sequences and series

HasProd.int_rec

∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousMul M] {f g : ℕ → M},
  HasProd f m → HasProd g m' → HasProd (fun t => Int.rec f g t) (m * m')

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.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.NatInt

Cited by

1 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidTopologicalSpaceContinuousMul