Even power of -1

Stream: Is there code for X?

[Yaël Dillies]

Do we really not have this? Maybe @Damiano Testa knows?

import algebra.parity

example {R : Type*} [ring R] {n : ℕ} (h : even n) : (-1 : R) ^ n = 1 := sorry

example {R : Type*} [ring R] {n : ℕ} (h : even n) (a : R) : (-a : R) ^ n = a ^n := sorry

[Riccardo Brasca]

docs#nat.neg_one_pow_of_even

[Eric Rodriguez]

docs#neg_one_pow_eq_pow_mod_two, docs#nat.neg_one_pow_eq_one_iff_even

[Yaël Dillies]

Ugh, that's a terrible name :sad:

[Eric Wieser]

The second name of the three, I assume?

[Yaël Dillies]

The first one. I was looking for even.neg_one_pow, even.neg_pow, ...

[Eric Wieser]

Good point, we don't usually put things about natural powers in the nat namespace

[Eric Rodriguez]

oh, I assumed it was about nat-powers! dear lord...

[Yaël Dillies]

Ah yes, -1 : nat :rolling_on_the_floor_laughing:

[Yaël Dillies]

I will issue a PR to fix the name today.

[Eric Rodriguez]

Yaël Dillies said:

Ah yes, -1 : nat :rolling_on_the_floor_laughing:

404: my brain cannot be located today :shock:

[Yaël Dillies]

#13268

[Yaël Dillies]

I'm cleaning up a few other things simultaneously. Maybe @Damiano Testa wants to have a look.

[Stuart Presnell]

We've transcended the boring debate over whether 0 should be included in the natural numbers, and moved on to whether -1 should be included :smile:

[Eric Rodriguez]

Yaël Dillies said:

#13268

literally above your post on Zulip is bors merging my generalisation of the typeclasses in that file, sorry about that!

[Damiano Testa]

Yaël, I left a review: I'm on mobile, so have not been able to experiment, but it all looks fine!

Regarding odd, especially in view of what its to_multiplicative version should be, I think that, if we really want to define it in general, it should be "not even". Having said this, I'm not sure that it is such a useful concept when it does not also mean 2*x+1 (or x+x+1 :wink: ), which I'm not sure how to multiplicativize.