(-1)^i

Stream: maths

[Johan Commelin]

Given i : nat, an additive commutative group A, and a : A, I want to talk about (-1)^i a. Is there already something in mathlib that does that? Or should I roll my own thing?
I guess I could take the i-th composite of neg with itself, and apply that to a. But is that the appropriate thing to do?

[Chris Hughes]

add_group.gsmul ((-1) ^i) a I think