division of big operator

Stream: new members

[Sophia Rodriguez]

Hi guys, I want to prove

∏ x ∈ s, f x / g x = (∏ x ∈ s, f x) / ∏ x ∈ s, g x

where s is a finset and bothf x& g x are nonzero natural number through out s. I discovered a thing called Finset.prod_div_distrib in mathlib but it asks me to fill in a DivisionCommMonoid, what can I do to resolve this?

[Junyan Xu]

You probably want to insert some type ascriptions like (f x / g x : ℚ) to ensure all divisions are applied to rational numbers. Otherwise, you get 1 / 2 = 0 etc. (And ℚ is a field and therefore a DivisionCommMonoid.)

[Sophia Rodriguez]

Okay, didn't think of that. I'll try, thanks