Zulip Chat Archive

Stream: maths

Topic: (-1)^i

view this post on Zulip Johan Commelin (Nov 21 2018 at 18:58):

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?

view this post on Zulip Chris Hughes (Nov 21 2018 at 19:00):

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

Last updated: May 19 2021 at 00:40 UTC