ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>g : M ≃+ N<VAR>f : α → M<GOAL>g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
<VAR>ι : Sort u_6<VAR>R : Type u_7<VAR>M : Type u_8<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>f : ι → R<VAR>x : M<GOAL>(∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
<VAR>ι : Sort u_6<VAR>R : Type u_7<VAR>M : Type u_8<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>c : R<VAR>f : ι → M<GOAL>c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
<VAR>G : Type u_1<VAR>α : Sort u_4<VAR>DivisionCommMonoid G<VAR>f : α → G<GOAL>∏ᶠ (x : α), (f x)⁻¹ = (∏ᶠ (x : α), f x)⁻¹
<VAR>G : Type u_1<VAR>α : Sort u_4<VAR>SubtractionCommMonoid G<VAR>f : α → G<GOAL>∑ᶠ (x : α), -f x = -∑ᶠ (x : α), f x
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>∑ᶠ (_ : a ∈ s), f a = s.indicator f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (_ : f a ≠ 1), f a = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∑ᶠ (_ : f a ≠ 0), f a = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<VAR>f : α → M<GOAL>∑ᶠ (a : α) (_ : a ∈ s), f a = ∑ᶠ (a : α), s.indicator f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<VAR>f : α → M<GOAL>∏ᶠ (a : α) (_ : a ∈ s), f a = ∏ᶠ (a : α), s.mulIndicator f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Finset α<VAR>h : Function.mulSupport f ⊆ ↑s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Finset α<VAR>h : Function.support f ⊆ ↑s<GOAL>∑ᶠ (i : α), f i = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>hf : (Function.support f).Finite<VAR>s : Finset α<VAR>h : hf.toFinset ⊆ s<GOAL>∑ᶠ (i : α), f i = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>hf : (Function.mulSupport f).Finite<VAR>s : Finset α<VAR>h : hf.toFinset ⊆ s<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>Decidable (Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α), f i = if h : (Function.mulSupport f).Finite then ∏ i ∈ h.toFinset, f i else 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>Decidable (Function.support f).Finite<GOAL>∑ᶠ (i : α), f i = if h : (Function.support f).Finite then ∑ i ∈ h.toFinset, f i else 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>hf : (Function.mulSupport f).Infinite<GOAL>∏ᶠ (i : α), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>hf : (Function.support f).Infinite<GOAL>∑ᶠ (i : α), f i = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α), f i = ∏ i ∈ hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>hf : (Function.support f).Finite<GOAL>∑ᶠ (i : α), f i = ∑ i ∈ hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>Fintype α<VAR>f : α → M<GOAL>∑ᶠ (i : α), f i = ∑ i : α, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>Fintype α<VAR>f : α → M<GOAL>∏ᶠ (i : α), f i = ∏ i : α, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 1 → (p x ↔ x ∈ t)<GOAL>∏ᶠ (i : α) (_ : p i), f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>p : α → Prop<VAR>t : Finset α<VAR>h : ∀ {x : α}, f x ≠ 0 → (p x ↔ x ∈ t)<GOAL>∑ᶠ (i : α) (_ : p i), f i = ∑ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>DecidableEq α<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ≠ a), f i = ∏ i ∈ hf.toFinset.erase a, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>DecidableEq α<VAR>hf : (Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ≠ a), f i = ∑ i ∈ hf.toFinset.erase a, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h : s ∩ Function.support f = ↑t ∩ Function.support f<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h : s ∩ Function.mulSupport f = ↑t ∩ Function.mulSupport f<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h₁ : s ∩ Function.support f ⊆ ↑t<VAR>h₂ : ↑t ⊆ s<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>t : Finset α<VAR>h₁ : s ∩ Function.mulSupport f ⊆ ↑t<VAR>h₂ : ↑t ⊆ s<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ t, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hf : (s ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hf : (s ∩ Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hf : (Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ Finset.filter (fun x => x ∈ s) hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hf : (Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ Finset.filter (fun x => x ∈ s) hf.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>Fintype ↑s<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ s.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>Fintype ↑s<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ s.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ hs.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ hs.toFinset, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Finset α<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Finset α<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Finset α<GOAL>∏ᶠ (i : α) (_ : i ∈ ↑s), f i = ∏ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Finset α<GOAL>∑ᶠ (i : α) (_ : i ∈ ↑s), f i = ∑ i ∈ s, f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hs : (s ∩ Function.mulSupport f).Infinite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hs : (s ∩ Function.support f).Infinite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∀ x ∈ s, f x = 0<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∀ x ∈ s, f x = 1<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∩ Function.mulSupport f), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∩ Function.support f), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>h : s ∩ Function.support f = t ∩ Function.support f<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>h : s ∩ Function.mulSupport f = t ∩ Function.mulSupport f<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>h : ∀ x ∈ Function.support f, x ∈ s ↔ x ∈ t<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>h : ∀ x ∈ Function.mulSupport f, x ∈ s ↔ x ∈ t<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>∑ᶠ (i : α) (_ : i ∈ Set.univ), f i = ∑ᶠ (i : α), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<GOAL>∏ᶠ (i : α) (_ : i ∈ Set.univ), f i = ∏ᶠ (i : α), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f g : α → M<VAR>s t : Set α<VAR>h₀ : s = t<VAR>h₁ : ∀ x ∈ t, f x = g x<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>s t : Set α<VAR>h₀ : s = t<VAR>h₁ : ∀ x ∈ t, f x = g x<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>h : ∀ (x : α), f x = 1<GOAL>∏ᶠ (i : α), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>h : ∀ (x : α), f x = 0<GOAL>∑ᶠ (i : α), f i = 0
<VAR>ι : Type u_3<VAR>M : Type u_7<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>h : ∀ (i : ι), 1 ≤ f i<VAR>h' : ∃ i, 1 < f i<VAR>hf : (Function.mulSupport f).Finite<GOAL>1 < ∏ᶠ (i : ι), f i
<VAR>ι : Type u_3<VAR>M : Type u_7<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>h : ∀ (i : ι), 0 ≤ f i<VAR>h' : ∃ i, 0 < f i<VAR>hf : (Function.support f).Finite<GOAL>0 < ∑ᶠ (i : ι), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f g : α → M<VAR>hf : (Function.mulSupport f).Finite<VAR>hg : (Function.mulSupport g).Finite<GOAL>∏ᶠ (i : α), f i * g i = (∏ᶠ (i : α), f i) * ∏ᶠ (i : α), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>hf : (Function.support f).Finite<VAR>hg : (Function.support g).Finite<GOAL>∑ᶠ (i : α), (f i + g i) = ∑ᶠ (i : α), f i + ∑ᶠ (i : α), g i
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>DivisionCommMonoid G<VAR>f g : α → G<VAR>hf : (Function.mulSupport f).Finite<VAR>hg : (Function.mulSupport g).Finite<GOAL>∏ᶠ (i : α), f i / g i = (∏ᶠ (i : α), f i) / ∏ᶠ (i : α), g i
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>SubtractionCommMonoid G<VAR>f g : α → G<VAR>hf : (Function.support f).Finite<VAR>hg : (Function.support g).Finite<GOAL>∑ᶠ (i : α), (f i - g i) = ∑ᶠ (i : α), f i - ∑ᶠ (i : α), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>s : Set α<VAR>hf : (s ∩ Function.support f).Finite<VAR>hg : (s ∩ Function.support g).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), (f i + g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f g : α → M<VAR>s : Set α<VAR>hf : (s ∩ Function.mulSupport f).Finite<VAR>hg : (s ∩ Function.mulSupport g).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<GOAL>∑ᶠ (i : α) (_ : i ∈ s), 0 = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<GOAL>∏ᶠ (i : α) (_ : i ∈ s), 1 = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hf : Set.EqOn f 0 s<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>hf : Set.EqOn f 1 s<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∑ᶠ (i : α) (_ : i ∈ s), f i ≠ 0<GOAL>∃ x ∈ s, f x ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1<GOAL>∃ x ∈ s, f x ≠ 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f g : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i * g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f g : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), (f i + g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>f : α → M<VAR>g : M →* N<VAR>hf : (Function.mulSupport f).Finite<GOAL>g (∏ᶠ (i : α), f i) = ∏ᶠ (i : α), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>f : α → M<VAR>g : M →+ N<VAR>hf : (Function.support f).Finite<GOAL>g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>hf : (Function.support f).Finite<VAR>n : ℕ<GOAL>n • ∑ᶠ (i : α), f i = ∑ᶠ (i : α), n • f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>hf : (Function.mulSupport f).Finite<VAR>n : ℕ<GOAL>(∏ᶠ (i : α), f i) ^ n = ∏ᶠ (i : α), f i ^ n
<VAR>ι : Type u_3<VAR>R : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : ι → R<VAR>hf : (Function.support f).Finite<VAR>x : M<GOAL>(∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
<VAR>ι : Type u_3<VAR>R : Type u_7<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>c : R<VAR>f : ι → M<VAR>hf : (Function.support f).Finite<GOAL>c • ∑ᶠ (i : ι), f i = ∑ᶠ (i : ι), c • f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>s : Set α<VAR>f : α → M<VAR>g : M →* N<VAR>h₀ : (s ∩ Function.mulSupport f).Finite<GOAL>g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>s : Set α<VAR>f : α → M<VAR>g : M →+ N<VAR>h₀ : (s ∩ Function.support f).Finite<GOAL>g (∑ᶠ (j : α) (_ : j ∈ s), f j) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>s : Set α<VAR>f : α → M<VAR>g : M →+ N<VAR>hs : s.Finite<GOAL>g (∑ᶠ (j : α) (_ : j ∈ s), f j) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>s : Set α<VAR>f : α → M<VAR>g : M →* N<VAR>hs : s.Finite<GOAL>g (∏ᶠ (j : α) (_ : j ∈ s), f j) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>g : M ≃* N<VAR>f : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>g (∏ᶠ (i : α) (_ : i ∈ s), f i) = ∏ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>g : M ≃+ N<VAR>f : α → M<VAR>s : Set α<VAR>hs : s.Finite<GOAL>g (∑ᶠ (i : α) (_ : i ∈ s), f i) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>s : Set α<VAR>SubtractionCommMonoid G<VAR>f : α → G<VAR>hs : s.Finite<GOAL>∑ᶠ (x : α) (_ : x ∈ s), -f x = -∑ᶠ (x : α) (_ : x ∈ s), f x
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>s : Set α<VAR>DivisionCommMonoid G<VAR>f : α → G<VAR>hs : s.Finite<GOAL>∏ᶠ (x : α) (_ : x ∈ s), (f x)⁻¹ = (∏ᶠ (x : α) (_ : x ∈ s), f x)⁻¹
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>s : Set α<VAR>SubtractionCommMonoid G<VAR>f g : α → G<VAR>hs : s.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s), (f i - g i) = ∑ᶠ (i : α) (_ : i ∈ s), f i - ∑ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>G : Type u_4<VAR>s : Set α<VAR>DivisionCommMonoid G<VAR>f g : α → G<VAR>hs : s.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i / g i = (∏ᶠ (i : α) (_ : i ∈ s), f i) / ∏ᶠ (i : α) (_ : i ∈ s), g i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<GOAL>∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>∑ᶠ (i : α) (_ : i ∈ ∅), f i = 0
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set α<VAR>h : ∑ᶠ (i : α) (_ : i ∈ s), f i ≠ 0<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i + ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hs : (s ∩ Function.support f).Finite<VAR>ht : (t ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i + ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hs : (s ∩ Function.mulSupport f).Finite<VAR>ht : (t ∩ Function.mulSupport f).Finite<GOAL>(∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : (s ∩ Function.support f).Finite<VAR>ht : (t ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : (s ∩ Function.mulSupport f).Finite<VAR>ht : (t ∩ Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint s t<VAR>hs : s.Finite<VAR>ht : t.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint (s ∩ Function.support f) (t ∩ Function.support f)<VAR>hs : (s ∩ Function.support f).Finite<VAR>ht : (t ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s t : Set α<VAR>hst : Disjoint (s ∩ Function.mulSupport f) (t ∩ Function.mulSupport f)<VAR>hs : (s ∩ Function.mulSupport f).Finite<VAR>ht : (t ∩ Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ s ∪ t), f i = (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∑ᶠ (i : α) (_ : i ∈ {a}), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (i : α) (_ : i ∈ {a}), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (i : α) (_ : i = a), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∑ᶠ (i : α) (_ : i = a), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∑ᶠ (i : α) (_ : a = i), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<GOAL>∏ᶠ (i : α) (_ : a = i), f i = f a
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : (s ∩ Function.support f).Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ insert a s), f i = f a + ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : (s ∩ Function.mulSupport f).Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : s.Finite<GOAL>∑ᶠ (i : α) (_ : i ∈ insert a s), f i = f a + ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>a : α<VAR>s : Set α<VAR>f : α → M<VAR>h : a ∉ s<VAR>hs : s.Finite<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s → f a = 1<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : Set α<VAR>h : a ∉ s → f a = 0<GOAL>∑ᶠ (i : α) (_ : i ∈ insert a s), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : Set α<VAR>h : f a = 0<GOAL>∑ᶠ (i : α) (_ : i ∈ insert a s), f i = ∑ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a : α<VAR>s : Set α<VAR>h : f a = 1<GOAL>∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
<VAR>α : Type u_1<VAR>N : Type u_6<VAR>CommMonoid N<VAR>f : α → N<VAR>a : α<VAR>hf : (Function.mulSupport f).Finite<GOAL>f a ∣ finprod f
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>h : a ≠ b<GOAL>∑ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a + f b
<VAR>α : Type u_1<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>h : a ≠ b<GOAL>∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<VAR>hg : Set.InjOn g (s ∩ Function.support (f ∘ g))<GOAL>∑ᶠ (i : α) (_ : i ∈ g '' s), f i = ∑ᶠ (j : β) (_ : j ∈ s), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<VAR>hg : Set.InjOn g (s ∩ Function.mulSupport (f ∘ g))<GOAL>∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<VAR>hg : Set.InjOn g s<GOAL>∑ᶠ (i : α) (_ : i ∈ g '' s), f i = ∑ᶠ (j : β) (_ : j ∈ s), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>s : Set β<VAR>g : β → α<VAR>hg : Set.InjOn g s<GOAL>∏ᶠ (i : α) (_ : i ∈ g '' s), f i = ∏ᶠ (j : β) (_ : j ∈ s), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>g : β → α<VAR>hg : Set.InjOn g (Function.mulSupport (f ∘ g))<GOAL>∏ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∏ᶠ (j : β), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>g : β → α<VAR>hg : Set.InjOn g (Function.support (f ∘ g))<GOAL>∑ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∑ᶠ (j : β), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>f : α → M<VAR>g : β → α<VAR>hg : Function.Injective g<GOAL>∑ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∑ᶠ (j : β), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>g : β → α<VAR>hg : Function.Injective g<GOAL>∏ᶠ (i : α) (_ : i ∈ Set.range g), f i = ∏ᶠ (j : β), f (g j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Set α<VAR>t : Set β<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Set.BijOn e s t<VAR>he₁ : ∀ x ∈ s, f x = g (e x)<GOAL>∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Set α<VAR>t : Set β<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Set.BijOn e s t<VAR>he₁ : ∀ x ∈ s, f x = g (e x)<GOAL>∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ᶠ (j : β) (_ : j ∈ t), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_5<VAR>CommMonoid M<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Function.Bijective e<VAR>he₁ : ∀ (x : α), f x = g (e x)<GOAL>∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j