## Stream: new members

### Topic: zmod neg_one

#### Damiano Testa (Apr 06 2021 at 16:09):

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 (Apr 06 2021 at 16:11):

This is false for n = 0 :sad:

#### Damiano Testa (Apr 06 2021 at 16:11):

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

#### Johan Commelin (Apr 06 2021 at 16:12):

Nope, that's zmod 1.

#### Damiano Testa (Apr 06 2021 at 16:12):

I thought that they were the same!

#### Johan Commelin (Apr 06 2021 at 16:12):

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

#### Damiano Testa (Apr 06 2021 at 16:12):

ah, so it is not finite!!

Ok, thanks!

#### Johan Commelin (Apr 06 2021 at 16:12):

You need [fact (0 < n)]

#### Damiano Testa (Apr 06 2021 at 16:14):

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 (Apr 06 2021 at 16:14):

(and, besides, is true?)

#### Damiano Testa (Apr 06 2021 at 16:14):

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

#### Damiano Testa (Apr 06 2021 at 16:15):

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

#### Kevin Buzzard (Apr 06 2021 at 16:15):

fin 0 has 0 elements!

#### Johan Commelin (Apr 06 2021 at 16:15):

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

#### Kevin Buzzard (Apr 06 2021 at 16:15):

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

#### Damiano Testa (Apr 06 2021 at 16:16):

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 (Apr 07 2021 at 05:27):

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)


Last updated: May 11 2021 at 13:22 UTC