Zulip Chat Archive

Stream: maths

Topic: pow_pow


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 14 2018 at 13:32):

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

view this post on Zulip Mario Carneiro (Nov 14 2018 at 13:33):

I agree that both directions have some claim to reasonableness

view this post on Zulip Kevin Buzzard (Nov 14 2018 at 13:34):

So the left-arrow is fine?


Last updated: May 09 2021 at 09:11 UTC