zmod neg_one

Stream: new members

[Damiano Testa]

Dear All,

is the lemma below already in mathlib, in one form or another?

Thanks!

import data.zmod.basic

lemma zmod.pred_eq_neg_one (n : ℕ) : ((n.pred) : zmod n) = - 1 :=
begin
  sorry
end

[Johan Commelin]

This is false for n = 0 :sad:

[Damiano Testa]

Is it? I thought that for n=0 zmod 0 was the zero ring, no?

[Johan Commelin]

Nope, that's zmod 1.

[Damiano Testa]

I thought that they were the same!

[Johan Commelin]

zmod 0 is $\Z/0\Z$. It's actually defeq to int

[Damiano Testa]

ah, so it is not finite!!

[Damiano Testa]

Ok, thanks!

[Johan Commelin]

You need [fact (0 < n)]

[Damiano Testa]

So, this one says what I think it does?

lemma zmod.pred_eq_neg_one (n : ℕ) [fact (0 < n)] : ((n.pred) : zmod n) = - 1 :=
begin
  sorry
end

[Damiano Testa]

(and, besides, is true?)

[Damiano Testa]

so, is it fin 0 that is the zero ring?

[Damiano Testa]

(or maybe fin 0 is even empty...)

[Kevin Buzzard]

fin 0 has 0 elements!

[Johan Commelin]

Yes, I think so. You can now prove it using cases n, and then discharge the first goal using the fact.

[Kevin Buzzard]

fin n has n elements, zmod n is Z/nZ.

[Damiano Testa]

Ok, I actually like these conventions! For some reasons, I was convinced that the conventions around zmod 0 and fin 0 were iffy... but they are not!

[Damiano Testa]

For completeness, here is a proof:

lemma zmod.pred_eq_neg_one (n : ℕ) [h : fact (0 < n)] : ((n.pred) : zmod n) = - 1 :=
begin
  casesI n,
  { exact (lt_irrefl 0 h.1).elim },
  { exact add_eq_zero_iff_eq_neg.mp (zmod.nat_cast_self' _) }
end

or even in equation compiler form:

lemma zmod.pred_eq_neg_one : ∀ (n : ℕ), 0 < n → (n.pred : zmod n) = - 1
| 0 h := (lt_irrefl 0 h).elim
| (n + 1) _ := add_eq_zero_iff_eq_neg.mp (zmod.nat_cast_self' n)