Johan Commelin (Nov 21 2018 at 18:58):
i : nat, an additive commutative group
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 (Nov 21 2018 at 19:00):
add_group.gsmul ((-1) ^i) a I think
Last updated: May 19 2021 at 00:40 UTC