power of product in comm_monoid

Stream: Is there code for X?

[Xavier Xarles]

I need this:

lemma pow_prod {G : Type}comm_monoid G(n:nat): (ab)^n=(a^n)*(b^n):=
sorry

I guess one should be able to prove using big_operators.findprod.finprod_pow

[Johan Commelin]

Should be mul_pow.

[Xavier Xarles]

ups, thanks, you are right.

[Eric Wieser]

For future reference, #backticks