Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC