-1 ^ n

Stream: Is there code for X?

[Andrew Yang]

Is this function defined anywhere in mathlib?

import data.int.parity
def foo (n : ℤ) : ℤ := if even n then 1 else -1

[Adam Topaz]

Does (-1)^(n % 2) work? Does a % b even exist?

[Adam Topaz]

Is the if .. then .. else .. form any better than just (-1)^n?

[Andrew Yang]

There doesn't seem to be a general has_pow ℤ ℤ since zero breaks things.
Or is there a type of nonzero integers?

[Eric Rodriguez]

hmm it doesn't have the support I thought; for \N you could easily swap between them both with docs#pow_eq_mod_order_of

[Adam Topaz]

Well, that would be has pow with Nat exponents.

[Eric Rodriguez]

you'd need Q for Z-powers?

[Adam Topaz]

If you take the remainder, that is.

[Adam Topaz]

And if you consider -1 as a unit Int, then you would be able to take integer powers

[Andrew Yang]

The type of % seems to be has_mod.mod : Π {α : Type} [self : has_mod α], α → α → α, so it still gives an int.
If there is also a proof that it is nonnegative, I might be able to cast it into a nat, but I'm not sure if it is easy to work with

[Eric Rodriguez]

I think the unit int idea may be a fruitful one

[Adam Topaz]

Yeah, you can take the power of the unit -1, then coerce back to an int

[Andrew Yang]

That works great. Thanks!
Is this map worthy of being added to mathlib?

[Eric Rodriguez]

fwiw, the only few instances I can find of a similar pattern in the library:

(I wrote this):

@[simp] lemma neg_one_geom_sum [ring α] {n : ℕ} : geom_sum (-1 : α) n = if even n then 0 else 1 :=

\+ it's also used in the definition of cos/sin. Meanwhile, I can't seem to find a single use of (-1)^(x : Z) anywhere

[Eric Rodriguez]

I think it'd be nice to have a few lemmas; but also, tbf, (-1) ^ nat_abs n works; maybe it's just worth adding that as a simp lemma