-1 raised to an integer

Stream: maths

[Enrico Borba]

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]

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]

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

[Enrico Borba]

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]

units ℤ isn't a ring

[Mario Carneiro]

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

[Enrico Borba]

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

[Scott Carnahan]

I'm not sure if I should make a new topic instead of joining a 3.5 year old conversation, but I thought I should note that I tried the above solution in mathlib4 without success. I was able to make things work with (-1: ℤˣ)^n but multiplying with elements of other rings seemed to require an additional cast, e.g., (((-1: ℤˣ)^n):ℤ)

[Anatole Dedecker]

Could you write a #mwe of what fails precisely?

[Kyle Miller]

You are probably looking for the local macro_rules | ($x ^ $y) => (HPow.hPow $x $y) workaround. Lean 4 has a system to try to cast everything in an arithmetic expression to a single type, but this doesn't work well for exponentiation at the moment. The macro_rules incantation turns this feature off for exponentiation.

[Scott Carnahan]

import Mathlib.Algebra.Module.Basic

#check (-1: ℤˣ)^(-2:ℤ )
#check (-1: units ℤ)^(-1:ℤ ) -- unknown identifier 'units'

Am I missing an import?

[Matthew Ballard]

It is Units in Lean 4

[Anatole Dedecker]

ℤˣ is Units ℤ by definition

[Scott Carnahan]

Oh, Units works. Thanks a lot!