ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>a b : α<VAR>s : Finset ι<GOAL>∑ t ∈ s.powerset, a ^ t.card * b ^ (s.card - t.card) = (a + b) ^ s.card
<VAR>α : Type u_2<VAR>CommSemiring α<VAR>ι : Type u_6<VAR>Fintype ι<VAR>a b : α<GOAL>∑ s : Finset ι, a ^ s.card * b ^ (Fintype.card ι - s.card) = (a + b) ^ Fintype.card ι
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommSemiring α<VAR>s : Finset ι<VAR>f : ι → ℕ<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommRing α<VAR>LinearOrder ι<VAR>s : Finset ι<VAR>f g : ι → α<GOAL>∏ i ∈ s, (f i - g i) = ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ Finset.filter (fun x => x < i) s, (f j - g j)) * ∏ j ∈ Finset.filter (fun j => i < j) s, f j
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommRing α<VAR>LinearOrder ι<VAR>s : Finset ι<VAR>f : ι → α<GOAL>∏ i ∈ s, (1 - f i) = 1 - ∑ i ∈ s, f i * ∏ j ∈ Finset.filter (fun x => x < i) s, (1 - f j)
<VAR>α : Type u_2<VAR>CommRing α<VAR>n k : ℕ<GOAL>∏ i ∈ Finset.range k, (↑n - ↑i) = ↑(∏ i ∈ Finset.range k, (n - i))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>DivisionSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>Fintype ι<VAR>CommSemiring α<VAR>f : ι → α<VAR>n : ℕ<GOAL>(∑ a : ι, f a) ^ n = ∑ p : Fin n → ι, ∏ i : Fin n, f (p i)
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>DecidableEq ι<VAR>CommSemiring α<VAR>κ : ι → Type u_9<VAR>Fintype ι<VAR>(i : ι) → Fintype (κ i)<VAR>f : (i : ι) → κ i → α<GOAL>∏ i : ι, ∑ j : κ i, f i j = ∑ x : (i : ι) → κ i, ∏ i : ι, f i (x i)
<VAR>ι : Type u_6<VAR>α : Type u_8<VAR>DecidableEq ι<VAR>Fintype ι<VAR>CommSemiring α<VAR>f g : ι → α<GOAL>∏ a : ι, (f a + g a) = ∑ t : Finset ι, (∏ a ∈ t, f a) * ∏ a ∈ tᶜ, g a
<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℕ<VAR>n : ℕ<VAR>hf : ∀ i ∈ s, n ∣ f i<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>β : Type u_3<VAR>AddMonoidWithOne β<VAR>s : List ℕ<GOAL>↑s.sum = (List.map Nat.cast s).sum
<VAR>β : Type u_3<VAR>Semiring β<VAR>s : List ℕ<GOAL>↑s.prod = (List.map Nat.cast s).prod
<VAR>β : Type u_3<VAR>AddCommMonoidWithOne β<VAR>s : Multiset ℕ<GOAL>↑s.sum = (Multiset.map Nat.cast s).sum
<VAR>β : Type u_3<VAR>CommSemiring β<VAR>s : Multiset ℕ<GOAL>↑s.prod = (Multiset.map Nat.cast s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommMonoidWithOne β<VAR>s : Finset α<VAR>f : α → ℕ<GOAL>↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>CommSemiring β<VAR>f : α → ℕ<VAR>s : Finset α<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>ι : Type u_6<VAR>s : Finset ι<VAR>f : ι → ℤ<VAR>n : ℤ<VAR>hf : ∀ i ∈ s, n ∣ f i<GOAL>(∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
<VAR>β : Type u_3<VAR>AddGroupWithOne β<VAR>s : List ℤ<GOAL>↑s.sum = (List.map Int.cast s).sum
<VAR>β : Type u_3<VAR>Ring β<VAR>s : List ℤ<GOAL>↑s.prod = (List.map Int.cast s).prod
<VAR>β : Type u_3<VAR>AddCommGroupWithOne β<VAR>s : Multiset ℤ<GOAL>↑s.sum = (Multiset.map Int.cast s).sum
<VAR>R : Type u_7<VAR>CommRing R<VAR>s : Multiset ℤ<GOAL>↑s.prod = (Multiset.map Int.cast s).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>AddCommGroupWithOne β<VAR>s : Finset α<VAR>f : α → ℤ<GOAL>↑(∑ x ∈ s, f x) = ∑ x ∈ s, ↑(f x)
<VAR>α : Type u_2<VAR>R : Type u_7<VAR>CommRing R<VAR>f : α → ℤ<VAR>s : Finset α<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>self : MixedCharZero R p<GOAL>∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>self : MixedCharZero R p<GOAL>CharZero R
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Prop<GOAL>(∀ p > 0, MixedCharZero R p → P) ↔ ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
<VAR>R : Type u_1<VAR>CommRing R<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>(∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p
<VAR>R : Type u_1<VAR>CommRing R<VAR>Algebra ℚ R<VAR>I : Ideal R<GOAL>I ≠ ⊤ → CharZero (R ⧸ I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>h : Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>IsUnit ↑↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))<VAR>n : ℕ+<GOAL>↑↑n = ↑↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<VAR>h : ∀ p > 0, ¬MixedCharZero R p<VAR>I : Ideal R<GOAL>I ≠ ⊤ → CharZero (R ⧸ I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)<VAR>p : ℕ<GOAL>p > 0 → ¬MixedCharZero R p
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<GOAL>(∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) ↔ ∀ p > 0, ¬MixedCharZero R p
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>CharZero R<GOAL>IsEmpty (Algebra ℚ R) ↔ ∃ p > 0, MixedCharZero R p
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Prop<VAR>CharZero R<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Prop<VAR>h_pos : ∀ (p : ℕ), p ≠ 0 → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Prop<VAR>IsDomain R<VAR>h_pos : ∀ (p : ℕ), Nat.Prime p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Prop<VAR>LocalRing R<VAR>h_pos : ∀ (p : ℕ), IsPrimePow p → CharP R p → P<VAR>h_equal : Algebra ℚ R → P<VAR>h_mixed : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P<GOAL>P
<VAR>u : Lean.Level<VAR>α : Q(Sort u)<VAR>a : Q(«$α»)<GOAL>«$a» =Q «$a»
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<GOAL>Multiset.lcm 0 = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).lcm = lcm a s.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>{a}.lcm = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ + s₂).lcm = lcm s₁.lcm s₂.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<GOAL>s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<GOAL>a ∣ s.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Multiset α<VAR>h : s₁ ⊆ s₂<GOAL>s₁.lcm ∣ s₂.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<GOAL>normalize s.lcm = s.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>Nontrivial α<VAR>s : Multiset α<GOAL>s.lcm = 0 ↔ 0 ∈ s
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup.lcm = s.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).lcm = lcm s₁.lcm s₂.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).lcm = lcm s₁.lcm s₂.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.ndinsert a s).lcm = lcm a s.lcm
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<GOAL>Multiset.gcd 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(a ::ₘ s).gcd = gcd a s.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<GOAL>{a}.gcd = normalize a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ + s₂).gcd = gcd s₁.gcd s₂.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<GOAL>a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>a : α<VAR>h : a ∈ s<GOAL>s.gcd ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s₁ s₂ : Multiset α<VAR>h : s₁ ⊆ s₂<GOAL>s₂.gcd ∣ s₁.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<GOAL>normalize s.gcd = s.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<GOAL>s.gcd = 0 ↔ ∀ x ∈ s, x = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.map (fun x => a * x) s).gcd = normalize a * s.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s : Multiset α<GOAL>s.dedup.gcd = s.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁.ndunion s₂).gcd = gcd s₁.gcd s₂.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>s₁ s₂ : Multiset α<GOAL>(s₁ ∪ s₂).gcd = gcd s₁.gcd s₂.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>DecidableEq α<VAR>a : α<VAR>s : Multiset α<GOAL>(Multiset.ndinsert a s).gcd = gcd a s.gcd
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s t : Multiset α<VAR>hs : ∃ x ∈ s, x ≠ 0<VAR>ht : s = Multiset.map (fun x => s.gcd * x) t<GOAL>t.gcd = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizedGCDMonoid α<VAR>s : Multiset α<VAR>hs : s ≠ 0<GOAL>∃ t, s = Multiset.map (fun x => s.gcd * x) t ∧ t.gcd = 1
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>s : Finset α<VAR>hs : f.support ⊆ s<VAR>g : α → M → N<VAR>h : ∀ i ∈ s, g i 0 = 1<GOAL>f.prod g = ∏ x ∈ s, g x (f x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>s : Finset α<VAR>hs : f.support ⊆ s<VAR>g : α → M → N<VAR>h : ∀ i ∈ s, g i 0 = 0<GOAL>f.sum g = ∑ x ∈ s, g x (f x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>Fintype α<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>h : ∀ (i : α), g i 0 = 0<GOAL>f.sum g = ∑ i : α, g i (f i)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>Fintype α<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>h : ∀ (i : α), g i 0 = 1<GOAL>f.prod g = ∏ i : α, g i (f i)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>a : α<VAR>b : M<VAR>h : α → M → N<VAR>h_zero : h a 0 = 1<GOAL>(Finsupp.single a b).prod h = h a b
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>a : α<VAR>b : M<VAR>h : α → M → N<VAR>h_zero : h a 0 = 0<GOAL>(Finsupp.single a b).sum h = h a b
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>Zero M<VAR>Zero M'<VAR>AddCommMonoid N<VAR>f : M → M'<VAR>hf : f 0 = 0<VAR>g : α →₀ M<VAR>h : α → M' → N<VAR>h0 : ∀ (a : α), h a 0 = 0<GOAL>(Finsupp.mapRange f hf g).sum h = g.sum fun a b => h a (f b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>Zero M<VAR>Zero M'<VAR>CommMonoid N<VAR>f : M → M'<VAR>hf : f 0 = 0<VAR>g : α →₀ M<VAR>h : α → M' → N<VAR>h0 : ∀ (a : α), h a 0 = 1<GOAL>(Finsupp.mapRange f hf g).prod h = g.prod fun a b => h a (f b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>h : α → M → N<GOAL>Finsupp.prod 0 h = 1
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>h : α → M → N<GOAL>Finsupp.sum 0 h = 0
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>Zero M<VAR>Zero M'<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>g : β →₀ M'<VAR>h : α → M → β → M' → N<GOAL>(f.prod fun x v => g.prod fun x' v' => h x v x' v') = g.prod fun x' v' => f.prod fun x v => h x v x' v'
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>Zero M<VAR>Zero M'<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g : β →₀ M'<VAR>h : α → M → β → M' → N<GOAL>(f.sum fun x v => g.sum fun x' v' => h x v x' v') = g.sum fun x' v' => f.sum fun x v => h x v x' v'
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(f.sum fun x v => if a = x then b x v else 0) = if a ∈ f.support then b a (f a) else 0
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(f.prod fun x v => if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>N : Type u_16<VAR>AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(f.sum fun x v => if a = x then v else 0) = f a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>N : Type u_16<VAR>AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(if a ∈ f.support then f a else 0) = f a
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(f.prod fun x v => if x = a then b x v else 1) = if a ∈ f.support then b a (f a) else 1
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>DecidableEq α<VAR>f : α →₀ M<VAR>a : α<VAR>b : α → M → N<GOAL>(f.sum fun x v => if x = a then b x v else 0) = if a ∈ f.support then b a (f a) else 0
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>N : Type u_16<VAR>AddCommMonoid N<VAR>f : α →₀ N<VAR>a : α<GOAL>(f.sum fun x v => if x = a then v else 0) = f a
<VAR>α : Type u_1<VAR>N : Type u_10<VAR>CommMonoid N<VAR>Fintype α<VAR>f : α →₀ ℕ<VAR>g : α → N<GOAL>(f.prod fun a b => g a ^ b) = ∏ a : α, g a ^ f a
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → M → N<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<VAR>hg : ∀ (a : α), g a 0 = 1<GOAL>(Finsupp.onFinset s f hf).prod g = ∏ a ∈ s, g a (f a)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>s : Finset α<VAR>f : α → M<VAR>g : α → M → N<VAR>hf : ∀ (a : α), f a ≠ 0 → a ∈ s<VAR>hg : ∀ (a : α), g a 0 = 0<GOAL>(Finsupp.onFinset s f hf).sum g = ∑ a ∈ s, g a (f a)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>y : α<VAR>g : α → M → N<VAR>hyf : y ∈ f.support<GOAL>g y (f y) * (Finsupp.erase y f).prod g = f.prod g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>y : α<VAR>g : α → M → N<VAR>hyf : y ∈ f.support<GOAL>g y (f y) + (Finsupp.erase y f).sum g = f.sum g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>y : α<VAR>g : α → M → N<VAR>hg : ∀ (i : α), g i 0 = 0<GOAL>g y (f y) + (Finsupp.erase y f).sum g = f.sum g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>y : α<VAR>g : α → M → N<VAR>hg : ∀ (i : α), g i 0 = 1<GOAL>g y (f y) * (Finsupp.erase y f).prod g = f.prod g
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>S : Type u_16<VAR>SetLike S N<VAR>AddSubmonoidClass S N<VAR>s : S<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>h : ∀ (c : α), f c ≠ 0 → g c (f c) ∈ s<GOAL>f.sum g ∈ s
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>S : Type u_16<VAR>SetLike S N<VAR>SubmonoidClass S N<VAR>s : S<VAR>f : α →₀ M<VAR>g : α → M → N<VAR>h : ∀ (c : α), f c ≠ 0 → g c (f c) ∈ s<GOAL>f.prod g ∈ s
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>g1 g2 : α → M → N<VAR>h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)<GOAL>f.prod g1 = f.prod g2
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g1 g2 : α → M → N<VAR>h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)<GOAL>f.sum g1 = f.sum g2
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>a : α<VAR>g : α → M → N<VAR>h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1<VAR>h₁ : f a = 0 → g a 0 = 1<GOAL>f.prod g = g a (f a)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>a : α<VAR>g : α → M → N<VAR>h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 0<VAR>h₁ : f a = 0 → g a 0 = 0<GOAL>f.sum g = g a (f a)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_7<VAR>Zero α<VAR>CommMonoidWithZero β<VAR>Nontrivial β<VAR>NoZeroDivisors β<VAR>f : ι →₀ α<VAR>g : ι → α → β<GOAL>f.prod g = 0 ↔ ∃ i ∈ f.support, g i (f i) = 0
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_7<VAR>Zero α<VAR>CommMonoidWithZero β<VAR>Nontrivial β<VAR>NoZeroDivisors β<VAR>f : ι →₀ α<VAR>g : ι → α → β<GOAL>f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero M<VAR>CommMonoid N<VAR>CommMonoid P<VAR>H : Type u_16<VAR>FunLike H N P<VAR>MonoidHomClass H N P<VAR>h : H<VAR>f : α →₀ M<VAR>g : α → M → N<GOAL>h (f.prod g) = f.prod fun a b => h (g a b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>H : Type u_16<VAR>FunLike H N P<VAR>AddMonoidHomClass H N P<VAR>h : H<VAR>f : α →₀ M<VAR>g : α → M → N<GOAL>h (f.sum g) = f.sum fun a b => h (g a b)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero β<VAR>AddMonoid N<VAR>AddCommMonoid P<VAR>f : α →₀ β<VAR>g : α → β → N →+ P<GOAL>⇑(f.sum g) = f.sum fun i fi => ⇑(g i fi)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero β<VAR>Monoid N<VAR>CommMonoid P<VAR>f : α →₀ β<VAR>g : α → β → N →* P<GOAL>⇑(f.prod g) = f.prod fun i fi => ⇑(g i fi)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero β<VAR>AddMonoid N<VAR>AddCommMonoid P<VAR>f : α →₀ β<VAR>g : α → β → N →+ P<VAR>x : N<GOAL>(f.sum g) x = f.sum fun i fi => (g i fi) x
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>N : Type u_10<VAR>P : Type u_11<VAR>Zero β<VAR>Monoid N<VAR>CommMonoid P<VAR>f : α →₀ β<VAR>g : α → β → N →* P<VAR>x : N<GOAL>(f.prod g) x = f.prod fun i fi => (g i fi) x
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>s : Multiset M<VAR>a : α<GOAL>Finsupp.single a s.sum = (Multiset.map (Finsupp.single a) s).sum
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → M<VAR>a : α<GOAL>Finsupp.single a (∑ b ∈ s, f b) = ∑ b ∈ s, Finsupp.single a (f b)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>s : ι →₀ M<VAR>f : ι → M → N<VAR>a : α<GOAL>Finsupp.single a (s.sum f) = s.sum fun d c => Finsupp.single a (f d c)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>G : Type u_12<VAR>AddGroup G<VAR>CommMonoid M<VAR>g : α →₀ G<VAR>h : α → G → M<VAR>h0 : ∀ (a : α), h a 0 = 1<GOAL>(-g).prod h = g.prod fun a b => h a (-b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>G : Type u_12<VAR>AddGroup G<VAR>AddCommMonoid M<VAR>g : α →₀ G<VAR>h : α → G → M<VAR>h0 : ∀ (a : α), h a 0 = 0<GOAL>(-g).sum h = g.sum fun a b => h a (-b)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>N : Type u_10<VAR>AddCommMonoid N<VAR>S : Finset ι<VAR>f : ι → α →₀ N<VAR>a : α<GOAL>(∑ i ∈ S, f i) a = ∑ i ∈ S, (f i) a
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → β →₀ N<VAR>a₂ : β<GOAL>(f.sum g) a₂ = f.sum fun a₁ b => (g a₁ b) a₂
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>N : Type u_10<VAR>AddCommMonoid N<VAR>S : Finset ι<VAR>f : ι → α →₀ N<GOAL>⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → β →₀ N<GOAL>⇑(f.sum g) = f.sum fun a₁ b => ⇑(g a₁ b)
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>N : Type u_10<VAR>DecidableEq β<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>g : α → M → β →₀ N<GOAL>(f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support
<VAR>α : Type u_1<VAR>β : Type u_7<VAR>M : Type u_8<VAR>DecidableEq β<VAR>AddCommMonoid M<VAR>s : Finset α<VAR>f : α → β →₀ M<GOAL>(s.sum f).support ⊆ s.biUnion fun x => (f x).support
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<GOAL>(f.sum fun x x => 0) = 0
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>AddCommMonoid N<VAR>f : α →₀ M<VAR>h₁ h₂ : α → M → N<GOAL>(f.sum fun a b => h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>Zero M<VAR>CommMonoid N<VAR>f : α →₀ M<VAR>h₁ h₂ : α → M → N<GOAL>(f.prod fun a b => h₁ a b * h₂ a b) = f.prod h₁ * f.prod h₂
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>G : Type u_12<VAR>Zero M<VAR>CommGroup G<VAR>f : α →₀ M<VAR>h : α → M → G<GOAL>(f.prod fun a b => (h a b)⁻¹) = (f.prod h)⁻¹
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>G : Type u_12<VAR>Zero M<VAR>AddCommGroup G<VAR>f : α →₀ M<VAR>h : α → M → G<GOAL>(f.sum fun a b => -h a b) = -f.sum h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>G : Type u_12<VAR>Zero M<VAR>AddCommGroup G<VAR>f : α →₀ M<VAR>h₁ h₂ : α → M → G<GOAL>(f.sum fun a b => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>DecidableEq α<VAR>AddZeroClass M<VAR>CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1<VAR>h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>(f + g).prod h = f.prod h * g.prod h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>DecidableEq α<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0<VAR>h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂<GOAL>(f + g).sum h = f.sum h + g.sum h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddZeroClass M<VAR>CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 1<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂<GOAL>(f + g).prod h = f.prod h * g.prod h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M → N<VAR>h_zero : ∀ (a : α), h a 0 = 0<VAR>h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂<GOAL>(f + g).sum h = f.sum h + g.sum h
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddZeroClass M<VAR>AddCommMonoid N<VAR>f g : α →₀ M<VAR>h : α → M →+ N<GOAL>((f + g).sum fun x => ⇑(h x)) = (f.sum fun x => ⇑(h x)) + g.sum fun x => ⇑(h x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddZeroClass M<VAR>CommMonoid N<VAR>f g : α →₀ M<VAR>h : α → Multiplicative M →* N<GOAL>((f + g).prod fun a b => (h a) (Multiplicative.ofAdd b)) = (f.prod fun a b => (h a) (Multiplicative.ofAdd b)) * g.prod fun a b => (h a) (Multiplicative.ofAdd b)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>F : α → M →+ N<VAR>f : α →₀ M<GOAL>(Finsupp.liftAddHom F) f = f.sum fun x => ⇑(F x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>F : (α →₀ M) →+ N<VAR>x : α<GOAL>Finsupp.liftAddHom.symm F x = F.comp (Finsupp.singleAddHom x)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>N : Type u_10<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>F : (α →₀ M) →+ N<VAR>x : α<VAR>y : M<GOAL>(Finsupp.liftAddHom.symm F x) y = F (Finsupp.single x y)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<GOAL>Finsupp.liftAddHom Finsupp.singleAddHom = AddMonoidHom.id (α →₀ M)
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>f : α →₀ M<GOAL>f.sum Finsupp.single = f
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : α →₀ M<GOAL>∑ a : α, Finsupp.single a (f a) = f
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Fintype α<VAR>i : α<VAR>m : M<GOAL>∑ j : α, (Finsupp.single i m) j = m
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Fintype α<VAR>i : α<VAR>m : M<GOAL>∑ j : α, (Finsupp.single j m) i = m
<VAR>α : Type u_1<VAR>M : Type u_8<VAR>Fintype α<VAR>AddCommMonoid M<VAR>f : α → M<GOAL>Finsupp.equivFunOnFinite.symm f = ∑ a : α, Finsupp.single a (f a)