## Stream: maths

### Topic: pow_pow

#### Kevin Buzzard (Nov 14 2018 at 13:29):

I just spent 60 seconds looking for pow_pow : (a ^ b) ^ c = a ^ (b * c) for a tactic mode rewrite, before I realised that it was actually called ←pow_mul. I'm always a little worried when I see those ← signs, it feels like I'm not going in the recommended direction. Is there a case for pow_pow?

#### Mario Carneiro (Nov 14 2018 at 13:32):

it's not a simp lemma, so you can use it whichever way you want to

#### Mario Carneiro (Nov 14 2018 at 13:33):

I agree that both directions have some claim to reasonableness

#### Kevin Buzzard (Nov 14 2018 at 13:34):

So the left-arrow is fine?

Last updated: May 09 2021 at 09:11 UTC