ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>AddGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>𝔖 : Set (Set α)<VAR>h𝔖₁ : 𝔖.Nonempty<VAR>h𝔖₂ : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<GOAL>(𝓝 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓝 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>f : ℕ → M<VAR>h : HasProd f m<GOAL>Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (𝓝 m)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>f : ℕ → M<VAR>h : HasSum f m<GOAL>Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 m)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>f : ℕ → M<VAR>h : Multipliable f<GOAL>Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (𝓝 (∏' (i : ℕ), f i))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>f : ℕ → M<VAR>h : Summable f<GOAL>Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 (∑' (i : ℕ), f i))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : HasSum (fun n => f (n + k)) m<GOAL>HasSum f (∑ i ∈ Finset.range k, f i + m)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : HasProd (fun n => f (n + k)) m<GOAL>HasProd f ((∏ i ∈ Finset.range k, f i) * m)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>h : HasProd (fun n => f (n + 1)) m<GOAL>HasProd f (f 0 * m)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>h : HasSum (fun n => f (n + 1)) m<GOAL>HasSum f (f 0 + m)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>he : HasSum (fun k => f (2 * k)) m<VAR>ho : HasSum (fun k => f (2 * k + 1)) m'<GOAL>HasSum f (m + m')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>he : HasProd (fun k => f (2 * k)) m<VAR>ho : HasProd (fun k => f (2 * k + 1)) m'<GOAL>HasProd f (m * m')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>T2Space M<VAR>f : ℕ → M<VAR>hf : Multipliable f<GOAL>HasProd f m ↔ Filter.Tendsto (fun n => ∏ i ∈ Finset.range n, f i) Filter.atTop (𝓝 m)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>T2Space M<VAR>f : ℕ → M<VAR>hf : Summable f<GOAL>HasSum f m ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (𝓝 m)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : Summable fun n => f (n + k)<GOAL>Summable f
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : Multipliable fun n => f (n + k)<GOAL>Multipliable f
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>he : Multipliable fun k => f (2 * k)<VAR>ho : Multipliable fun k => f (2 * k + 1)<GOAL>Multipliable f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>he : Summable fun k => f (2 * k)<VAR>ho : Summable fun k => f (2 * k + 1)<GOAL>Summable f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable β<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 0<VAR>s : β → α<GOAL>∑' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable β<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>s : β → α<GOAL>∏' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable β<VAR>m : Set α → M<VAR>m0 : m ∅ = 1<VAR>s : β → Set α<GOAL>∏' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Encodable β<VAR>m : Set α → M<VAR>m0 : m ∅ = 0<VAR>s : β → Set α<GOAL>∑' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∑' (b : β), m (s b)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Countable β<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : β → α<GOAL>R (m (⨆ b, s b)) (∏' (b : β), m (s b))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>β : Type u_4<VAR>Countable β<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 0<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))<VAR>s : β → α<GOAL>R (m (⨆ b, s b)) (∑' (b : β), m (s b))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>γ : Type u_5<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 0<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))<VAR>s : γ → α<VAR>t : Finset γ<GOAL>R (m (⨆ d ∈ t, s d)) (∑ d ∈ t, m (s d))
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>γ : Type u_5<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s : γ → α<VAR>t : Finset γ<GOAL>R (m (⨆ d ∈ t, s d)) (∏ d ∈ t, m (s d))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 0<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))<VAR>s₁ s₂ : α<GOAL>R (m (s₁ ⊔ s₂)) (m s₁ + m s₂)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>α : Type u_3<VAR>CompleteLattice α<VAR>m : α → M<VAR>m0 : m ⊥ = 1<VAR>R : M → M → Prop<VAR>m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))<VAR>s₁ s₂ : α<GOAL>R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : Multipliable fun n => f (n + k)<GOAL>(∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>k : ℕ<VAR>h : Summable fun n => f (n + k)<GOAL>∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>hf : Multipliable fun n => f (n + 1)<GOAL>∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>hf : Summable fun n => f (n + 1)<GOAL>∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousMul M<VAR>f : ℕ → M<VAR>he : Multipliable fun k => f (2 * k)<VAR>ho : Multipliable fun k => f (2 * k + 1)<GOAL>(∏' (k : ℕ), f (2 * k)) * ∏' (k : ℕ), f (2 * k + 1) = ∏' (k : ℕ), f k
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>ContinuousAdd M<VAR>f : ℕ → M<VAR>he : Summable fun k => f (2 * k)<VAR>ho : Summable fun k => f (2 * k + 1)<GOAL>∑' (k : ℕ), f (2 * k) + ∑' (k : ℕ), f (2 * k + 1) = ∑' (k : ℕ), f k
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>g : G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasSum (fun n => f (n + k)) g ↔ HasSum f (g + ∑ i ∈ Finset.range k, f i)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>g : G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasProd (fun n => f (n + k)) g ↔ HasProd f (g * ∏ i ∈ Finset.range k, f i)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>(Multipliable fun n => f (n + k)) ↔ Multipliable f
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>(Summable fun n => f (n + k)) ↔ Summable f
<VAR>G : Type u_2<VAR>CommGroup G<VAR>g : G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasProd (fun n => f (n + k)) (g / ∏ i ∈ Finset.range k, f i) ↔ HasProd f g
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>g : G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℕ → G<VAR>k : ℕ<GOAL>HasSum (fun n => f (n + k)) (g - ∑ i ∈ Finset.range k, f i) ↔ HasSum f g
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>f : ℕ → G<VAR>k : ℕ<VAR>h : Summable f<GOAL>∑ i ∈ Finset.range k, f i + ∑' (i : ℕ), f (i + k) = ∑' (i : ℕ), f i
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>f : ℕ → G<VAR>k : ℕ<VAR>h : Multipliable f<GOAL>(∏ i ∈ Finset.range k, f i) * ∏' (i : ℕ), f (i + k) = ∏' (i : ℕ), f i
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>f : ℕ → G<VAR>hf : Summable f<GOAL>∑' (b : ℕ), f b = f 0 + ∑' (b : ℕ), f (b + 1)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>f : ℕ → G<VAR>hf : Multipliable f<GOAL>∏' (b : ℕ), f b = f 0 * ∏' (b : ℕ), f (b + 1)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>f : ℕ → G<GOAL>Filter.Tendsto (fun i => ∏' (k : ℕ), f (k + i)) Filter.atTop (𝓝 1)
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>f : ℕ → G<GOAL>Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (𝓝 0)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>f : ℕ → G<GOAL>(CauchySeq fun s => ∏ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>f : ℕ → G<GOAL>(CauchySeq fun s => ∑ n ∈ s, f n) ↔ ∀ e ∈ 𝓝 0, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>CompleteSpace G<VAR>f : ℕ → G<GOAL>Summable f ↔ ∀ e ∈ 𝓝 0, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>CompleteSpace G<VAR>f : ℕ → G<GOAL>Multipliable f ↔ ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℕ → G<VAR>hf : Summable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 0<GOAL>∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℕ → G<VAR>hf : Multipliable f<VAR>e : Set G<VAR>he : e ∈ 𝓝 1<GOAL>∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℕ → G<VAR>hf : Summable f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 0)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℕ → G<VAR>hf : Multipliable f<GOAL>Filter.Tendsto f Filter.atTop (𝓝 1)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>f : ℤ → M<VAR>hf : HasSum f m<GOAL>HasSum (fun n => f ↑n + f (-(↑n + 1))) m
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>f : ℤ → M<VAR>hf : HasProd f m<GOAL>HasProd (fun n => f ↑n * f (-(↑n + 1))) m
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>f : ℤ → M<VAR>hf : Summable f<GOAL>Summable fun n => f ↑n + f (-(↑n + 1))
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>f : ℤ → M<VAR>hf : Multipliable f<GOAL>Multipliable fun n => f ↑n * f (-(↑n + 1))
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf : Multipliable f<GOAL>∏' (n : ℕ), f ↑n * f (-(↑n + 1)) = ∏' (n : ℤ), f n
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf : Summable f<GOAL>∑' (n : ℕ), (f ↑n + f (-(↑n + 1))) = ∑' (n : ℤ), f n
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf₁ : HasSum (fun n => f ↑n) m<VAR>hf₂ : HasSum (fun n => f (-(↑n + 1))) m'<GOAL>HasSum f (m + m')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf₁ : HasProd (fun n => f ↑n) m<VAR>hf₂ : HasProd (fun n => f (-(↑n + 1))) m'<GOAL>HasProd f (m * m')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf₁ : Multipliable fun n => f ↑n<VAR>hf₂ : Multipliable fun n => f (-(↑n + 1))<GOAL>Multipliable f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf₁ : Summable fun n => f ↑n<VAR>hf₂ : Summable fun n => f (-(↑n + 1))<GOAL>Summable f
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf₁ : Multipliable fun n => f ↑n<VAR>hf₂ : Multipliable fun n => f (-(↑n + 1))<GOAL>∏' (n : ℤ), f n = (∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-(↑n + 1))
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf₁ : Summable fun n => f ↑n<VAR>hf₂ : Summable fun n => f (-(↑n + 1))<GOAL>∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-(↑n + 1))
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousMul M<VAR>f g : ℕ → M<VAR>hf : HasProd f m<VAR>hg : HasProd g m'<GOAL>HasProd (fun t => Int.rec f g t) (m * m')
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousAdd M<VAR>f g : ℕ → M<VAR>hf : HasSum f m<VAR>hg : HasSum g m'<GOAL>HasSum (fun t => Int.rec f g t) (m + m')
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f g : ℕ → M<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>Summable fun t => Int.rec f g t
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f g : ℕ → M<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>Multipliable fun t => Int.rec f g t
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>T2Space M<VAR>f g : ℕ → M<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>∑' (n : ℤ), Int.rec f g n = ∑' (n : ℕ), f n + ∑' (n : ℕ), g n
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>T2Space M<VAR>f g : ℕ → M<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>∏' (n : ℤ), Int.rec f g n = (∏' (n : ℕ), f n) * ∏' (n : ℕ), g n
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf : HasSum f m<GOAL>HasSum (fun n => f ↑n + f (-↑n)) (m + f 0)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m : M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf : HasProd f m<GOAL>HasProd (fun n => f ↑n * f (-↑n)) (m * f 0)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf : Summable f<GOAL>Summable fun n => f ↑n + f (-↑n)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf : Multipliable f<GOAL>Multipliable fun n => f ↑n * f (-↑n)
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf : Summable f<GOAL>∑' (n : ℕ), (f ↑n + f (-↑n)) = ∑' (n : ℤ), f n + f 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf : Multipliable f<GOAL>∏' (n : ℕ), f ↑n * f (-↑n) = (∏' (n : ℤ), f n) * f 0
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf₁ : HasProd (fun n => f (↑n + 1)) m<VAR>hf₂ : HasProd (fun n => f (-(↑n + 1))) m'<GOAL>HasProd f (m * f 0 * m')
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>m m' : M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf₁ : HasSum (fun n => f (↑n + 1)) m<VAR>hf₂ : HasSum (fun n => f (-(↑n + 1))) m'<GOAL>HasSum f (m + f 0 + m')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>f : ℤ → M<VAR>hf₁ : Multipliable fun n => f (↑n + 1)<VAR>hf₂ : Multipliable fun n => f (-(↑n + 1))<GOAL>Multipliable f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>f : ℤ → M<VAR>hf₁ : Summable fun n => f (↑n + 1)<VAR>hf₂ : Summable fun n => f (-(↑n + 1))<GOAL>Summable f
<VAR>M : Type u_1<VAR>AddCommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousAdd M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf₁ : Summable fun n => f (↑n + 1)<VAR>hf₂ : Summable fun n => f (-(↑n + 1))<GOAL>∑' (n : ℤ), f n = ∑' (n : ℕ), f (↑n + 1) + f 0 + ∑' (n : ℕ), f (-(↑n + 1))
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>TopologicalSpace M<VAR>ContinuousMul M<VAR>T2Space M<VAR>f : ℤ → M<VAR>hf₁ : Multipliable fun n => f (↑n + 1)<VAR>hf₂ : Multipliable fun n => f (-(↑n + 1))<GOAL>∏' (n : ℤ), f n = (∏' (n : ℕ), f (↑n + 1)) * f 0 * ∏' (n : ℕ), f (-(↑n + 1))
<VAR>G : Type u_2<VAR>CommGroup G<VAR>g g' : G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℤ → G<VAR>hf₁ : HasProd (fun n => f ↑n) g<VAR>hf₂ : HasProd (fun n => f (-↑n)) g'<GOAL>HasProd f (g * g' / f 0)
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>g g' : G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℤ → G<VAR>hf₁ : HasSum (fun n => f ↑n) g<VAR>hf₂ : HasSum (fun n => f (-↑n)) g'<GOAL>HasSum f (g + g' - f 0)
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>f : ℤ → G<VAR>hf₁ : Multipliable fun n => f ↑n<VAR>hf₂ : Multipliable fun n => f (-↑n)<GOAL>Multipliable f
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>f : ℤ → G<VAR>hf₁ : Summable fun n => f ↑n<VAR>hf₂ : Summable fun n => f (-↑n)<GOAL>Summable f
<VAR>G : Type u_2<VAR>CommGroup G<VAR>TopologicalSpace G<VAR>TopologicalGroup G<VAR>T2Space G<VAR>f : ℤ → G<VAR>hf₁ : Multipliable fun n => f ↑n<VAR>hf₂ : Multipliable fun n => f (-↑n)<GOAL>∏' (n : ℤ), f n = ((∏' (n : ℕ), f ↑n) * ∏' (n : ℕ), f (-↑n)) / f 0
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>TopologicalSpace G<VAR>TopologicalAddGroup G<VAR>T2Space G<VAR>f : ℤ → G<VAR>hf₁ : Summable fun n => f ↑n<VAR>hf₂ : Summable fun n => f (-↑n)<GOAL>∑' (n : ℤ), f n = ∑' (n : ℕ), f ↑n + ∑' (n : ℕ), f (-↑n) - f 0
<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>CompleteSpace G<VAR>f : ℤ → G<GOAL>Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-(↑n + 1))
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>CompleteSpace G<VAR>f : ℤ → G<GOAL>Summable f ↔ (Summable fun n => f ↑n) ∧ Summable fun n => f (-(↑n + 1))
<VAR>G : Type u_2<VAR>CommGroup G<VAR>UniformSpace G<VAR>UniformGroup G<VAR>CompleteSpace G<VAR>f : ℤ → G<GOAL>Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-↑n)
<VAR>G : Type u_2<VAR>AddCommGroup G<VAR>UniformSpace G<VAR>UniformAddGroup G<VAR>CompleteSpace G<VAR>f : ℤ → G<GOAL>Summable f ↔ (Summable fun n => f ↑n) ∧ Summable fun n => f (-↑n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a : α<VAR>h : HasProd f a<GOAL>HasProd (fun b => (f b)⁻¹) a⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a : α<VAR>h : HasSum f a<GOAL>HasSum (fun b => -f b) (-a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>hf : Summable f<GOAL>Summable fun b => -f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>hf : Multipliable f<GOAL>Multipliable fun b => (f b)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>hf : Summable fun b => -f b<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>hf : Multipliable fun b => (f b)⁻¹<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<GOAL>(Summable fun b => -f b) ↔ Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<GOAL>(Multipliable fun b => (f b)⁻¹) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f g : β → α<VAR>a₁ a₂ : α<VAR>hf : HasProd f a₁<VAR>hg : HasProd g a₂<GOAL>HasProd (fun b => f b / g b) (a₁ / a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f g : β → α<VAR>a₁ a₂ : α<VAR>hf : HasSum f a₁<VAR>hg : HasSum g a₂<GOAL>HasSum (fun b => f b - g b) (a₁ - a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f g : β → α<VAR>hf : Multipliable f<VAR>hg : Multipliable g<GOAL>Multipliable fun b => f b / g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f g : β → α<VAR>hf : Summable f<VAR>hg : Summable g<GOAL>Summable fun b => f b - g b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f g : β → α<VAR>hg : Summable g<VAR>hfg : Summable fun b => f b - g b<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f g : β → α<VAR>hg : Multipliable g<VAR>hfg : Multipliable fun b => f b / g b<GOAL>Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f g : β → α<VAR>hfg : Multipliable fun b => f b / g b<GOAL>Multipliable f ↔ Multipliable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f g : β → α<VAR>hfg : Summable fun b => f b - g b<GOAL>Summable f ↔ Summable g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a₁ : α<VAR>hf : HasSum f a₁<VAR>b : β<VAR>DecidableEq β<VAR>a : α<GOAL>HasSum (Function.update f b a) (a - f b + a₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a₁ : α<VAR>hf : HasProd f a₁<VAR>b : β<VAR>DecidableEq β<VAR>a : α<GOAL>HasProd (Function.update f b a) (a / f b * a₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>hf : Multipliable f<VAR>b : β<VAR>DecidableEq β<VAR>a : α<GOAL>Multipliable (Function.update f b a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>hf : Summable f<VAR>b : β<VAR>DecidableEq β<VAR>a : α<GOAL>Summable (Function.update f b a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasSum (f ∘ Subtype.val) a₁<GOAL>HasSum (f ∘ Subtype.val) a₂ ↔ HasSum f (a₁ + a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (f ∘ Subtype.val) a₁<GOAL>HasProd (f ∘ Subtype.val) a₂ ↔ HasProd f (a₁ * a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasSum (f ∘ Subtype.val) a₁<GOAL>HasSum f a₂ ↔ HasSum (f ∘ Subtype.val) (a₂ - a₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>a₁ a₂ : α<VAR>s : Set β<VAR>hf : HasProd (f ∘ Subtype.val) a₁<GOAL>HasProd f a₂ ↔ HasProd (f ∘ Subtype.val) (a₂ / a₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CommGroup α<VAR>TopologicalSpace α<VAR>TopologicalGroup α<VAR>f : β → α<VAR>s : Set β<VAR>hf : Multipliable (f ∘ Subtype.val)<GOAL>Multipliable (f ∘ Subtype.val) ↔ Multipliable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>AddCommGroup α<VAR>TopologicalSpace α<VAR>TopologicalAddGroup α<VAR>f : β → α<VAR>s : Set β<VAR>hf : Summable (f ∘ Subtype.val)<GOAL>Summable (f ∘ Subtype.val) ↔ Summable f