Zulip Chat Archive

Stream: new members

Topic: zmod neg_one


view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 06 2021 at 16:11):

This is false for n = 0 :sad:

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:11):

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

view this post on Zulip Johan Commelin (Apr 06 2021 at 16:12):

Nope, that's zmod 1.

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:12):

I thought that they were the same!

view this post on Zulip Johan Commelin (Apr 06 2021 at 16:12):

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

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:12):

ah, so it is not finite!!

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:12):

Ok, thanks!

view this post on Zulip Johan Commelin (Apr 06 2021 at 16:12):

You need [fact (0 < n)]

view this post on Zulip 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

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:14):

(and, besides, is true?)

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:14):

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

view this post on Zulip Damiano Testa (Apr 06 2021 at 16:15):

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

view this post on Zulip Kevin Buzzard (Apr 06 2021 at 16:15):

fin 0 has 0 elements!

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 06 2021 at 16:15):

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

view this post on Zulip 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!

view this post on Zulip 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