## Stream: new members

### Topic: Surjection from Z into zmod

#### Hanting Zhang (Jan 03 2021 at 03:07):

Try as I might, I cannot complete this proof.

import data.zmod.basic

open function

example (n : ℕ) : surjective (algebra_map ℤ (zmod n)) :=
begin
unfold surjective,
intro,
use b.val,
simp only [int.cast_coe_nat, ring_hom.eq_int_cast],
-- n: ℕ
-- b: zmod n
-- ⊢ ↑(b.val) = b
sorry
end


How should I proceed?

#### Eric Wieser (Jan 03 2021 at 03:12):

Does ext help?

(deleted)

#### Hanting Zhang (Jan 03 2021 at 03:19):

No, zmod doesn't have ext. I guess what I'm really trying to do is identify zmod n with quotients of ℤ, but there seems to be no API for this.

#### Hanting Zhang (Jan 03 2021 at 03:20):

Maybe there is some sledgehammer to do this that I haven't found yet?

#### Alex J. Best (Jan 03 2021 at 03:26):

example (n : ℕ) : surjective (algebra_map ℤ (zmod n)) :=
begin
intro x,
use x,
cases n;
simp,
end


#### Alex J. Best (Jan 03 2021 at 03:27):

Its a bit weird because zmod n is defined quite differently for n=0 and n > 0, for n = 0 zmod n is just Z and for n positive it is fin n so sometimes you need to do cases on n for the proof to work.

#### Alex J. Best (Jan 03 2021 at 03:29):

I'd say the lemma

@[simp] lemma zmod.coe_coe_eq_self {n : ℕ} (a : zmod n) : ((a : ℤ) : zmod n) = a :=
by {cases n; simp}


#### Alex J. Best (Jan 03 2021 at 03:37):

Maybe more useful is for me to describe my process for finding the proof:
First I had, intro x and then use x.val like you did. Then I tried simp and the goal was ↑(x.val) = x so I tried the tactic norm_cast as there were up arrows in the goal, but it didn't help, so I thought maybe using val was not the right format for cast to work, so switched it to use x so that lean would insert a cast itself, so the goal after simp was then, ↑↑x = x so I tried library search, nothing happened so I searched mathlib for the string coe_coe and found a bunch of things including docs#fin.coe_coe_eq_self which seemed very useful. And so I thought that this lemma would work, as zmod is basically the same as fin, so I looked up the definition of zmod in mathlib and saw it split into two cases, so at that point I knew if I did cases on n then docs#fin.coe_coe_eq_self should apply to one case, and the other case might also be doable with simp.

#### Hanting Zhang (Jan 03 2021 at 03:41):

I see. Thanks for the explanation.

#### Hanting Zhang (Jan 03 2021 at 03:42):

Seeing your lemma, I tried to also do lemma zmod.coe_nat_coe_eq_self {n : ℕ} (a : zmod n) : ((a.val : ℕ) : zmod n) = a := by sorry, but this somehow does work?

#### Hanting Zhang (Jan 03 2021 at 03:48):

I think it's because Z is a ring, which might play better with zmod. This lemma doesn't really matter... but it would be nice to try to understand what's happening here.

#### Adam Topaz (Jan 03 2021 at 03:52):

This is a good exercise! But if you want to use it for something else, I suggest simply using docs#zmod.int_cast_surjective

#### Adam Topaz (Jan 03 2021 at 03:54):

The API for this stuff is somewhat extensive. You can find it in data.zmod.basic

#### Alex J. Best (Jan 03 2021 at 03:54):

I think the documentation of docs#zmod.cast is wrong in that it says you can cast to a semiring, but actually you need somewhere for -1 in zmod 0 to go with the current definition.

#### Adam Topaz (Jan 03 2021 at 03:56):

Should we make a natmod n :)

Last updated: May 15 2021 at 02:11 UTC