# Zulip Chat Archive

## 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!!

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

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: Dec 20 2023 at 11:08 UTC