Int.negOnePow vs (-1) ^ n

Stream: mathlib4

[Yury G. Kudryashov]

Do we have guidelines for using Int.negOnePow n vs (-1) ^ n? CC: @Johan Commelin #xy: which one should be used in #33972?

[Violeta Hernández]

What benefits does one have over the other? I imagine Int.negOnePow should work under much looser typeclass hypotheses, while (-1)^n comes with all the preexisting API for exponentiation.

[Violeta Hernández]

Maybe the rule should be that negOnePow n simps to (-1)^n over a group?

[Weiyi Wang]

I personally prefer (-1)^n when n is Nat, and Int.negOnePow when n is Int. (-1)^n is often easier to use, because e.g. ring tactic can handle it

[Michael Stoll]

docs#Int.negOnePow

[Weiyi Wang]

(I have #33143 that shows my preference)

[Eric Wieser]

Weiyi and Violeta; do you mean you prefer (-1 : ℤˣ) ^ n or (-1 : R) ^ n?

[Weiyi Wang]

I prefer the latter whenever it type-checks (unless the whole expression is in Z^x)

[Violeta Hernández]

I think I'd be inclined towards the former? But I don't have a strong preference here.

[Michael Stoll]

My totally uninformed take is that as a mathematician, I immediately understand what (-1) ^ n means, but parsing Int.negOnePow n or n.negOnePow takes a few seconds to process.

[Yury G. Kudryashov]

Let's wait for Johan. I don't see why Int.negOnePow is better than (-1 : ℤˣ) ^ n.

[Eric Wieser]

I think the idea of Int.negOnePow was to standardize on (-1 : ℤˣ) ^ n instead of (-1 : R) ^ n

[Yury G. Kudryashov]

I would use (-1 : R) ^ n for coercion (whenever it's defined).

[Eric Wieser]

By "for coercion" you mean "so as to avoid a coercion"?

[Yury G. Kudryashov]

I mean, instead of a coercion of Units Int to Int or other ring/field.

[Johan Commelin]

Sorry for my late response. I don't have a strong opinion on one or the other.
If I had one in the past, I should have documented it in the docstring on Int.negOnePow.

[Eric Wieser]

Perhaps the discussion on the original pr that added it has some context?

[Yury G. Kudryashov]

#6720

[Joël Riou]

As far as I can remember, I used Int.negOnePow in order to multiply certain morphisms in preadditive categories by signs as part of the formalization of homological algebra. There may have been issues with missing API regarding SMul ℤˣ M instances obtained from SMul ℤ M, but I do not remember the details. I would not mind if someone experimented making Int.negOnePow an abbrev (or removing it), while keeping certain lemmas (which may be generalized to other rings).