case empty
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
⊢ multiplicity p (∏ x in ∅, f x) = ∑ x in ∅, multiplicity p (f x)

case insert
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (∏ x in insert a s, f x) = ∑ x in insert a s, multiplicity p (f x)
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
induction' s using Finset.induction with a s has ih h
case empty
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
⊢ multiplicity p 1 = 0
case empty
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
⊢ multiplicity p (∏ x in ∅, f x) = ∑ x in ∅, multiplicity p (f x)
simp only [Finset.sum_empty, Finset.prod_empty]
no goals
case empty
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
⊢ multiplicity p 1 = 0
convert one_right hp.not_unit
case insert
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (f a * ∏ x in s, f x) = multiplicity p (f a) + multiplicity p (∏ x in s, f x)
case insert
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (∏ x in insert a s, f x) = ∑ x in insert a s, multiplicity p (f x)
simp [has, ← ih]
no goals
case insert
α : Type u_2
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
β : Type u_1
p : α
hp : Prime p
f : β → α
a : β
s : Finset β
has : ¬a ∈ s
ih : multiplicity p (∏ x in s, f x) = ∑ x in s, multiplicity p (f x)
⊢ multiplicity p (f a * ∏ x in s, f x) = multiplicity p (f a) + multiplicity p (∏ x in s, f x)
convert multiplicity.mul hp