Stream: maths

Topic: -1 raised to an integer

Enrico Borba (Jan 20 2020 at 17:28):

What's the best way of writing (-1) ^ n where n : int? You can't just write it as is since has_pow int int doesn't exist (and shouldn't of course). Is there some construct in mathlib for this?

Alex J. Best (Jan 20 2020 at 17:32):

I guess the best way depends on your application, but the reason -1 to a power is allowed is because -1 is a unit in the ring Z so one way would be

variable (n : ℤ)
#check (-1 : units ℤ) ^ n
#eval (-1 : units ℤ) ^ (-4 : ℤ)


Enrico Borba (Jan 20 2020 at 17:34):

Oh very interesting. I'll try this. Thank you

Enrico Borba (Jan 20 2020 at 20:31):

Hmm, is it obvious why ring_exp can't handle this?

example (n : ℕ) : ((-1 : units ℤ) ^ (n + 1)) = (-1 : units ℤ) * ((-1 : units ℤ) ^ n) := by ring_exp


Mario Carneiro (Jan 20 2020 at 20:39):

units ℤ isn't a ring

Mario Carneiro (Jan 20 2020 at 20:41):

it's also overkill for this example. There is a lemma that says exactly this; use library_search to find it

Enrico Borba (Jan 20 2020 at 20:54):

library_search suggests I just use rfl, which I guess makes sense depending on how pow is implemented on succ n. Thanks!

Last updated: May 14 2021 at 19:21 UTC