## Stream: new members

### Topic: Missing zmod lemma?

#### Michael Stoll (Mar 21 2022 at 19:22):

Not sure if this is the right stream for this question... (I'm still thinking of myself as a new member, though).
We have (in data.zmod.basic) the following

 theorem zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
theorem zmod.int_coe_eq_int_coe_iff' (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ a % ↑c = b % ↑c
theorem zmod.int_coe_zmod_eq_zero_iff_dvd (a : ℤ) (b : ℕ) : ↑a = 0 ↔ ↑b ∣ a


but I cannot seem to find

theorem zmod.int_coe_eq_int_coe_iff_dvd_sub (a b : ℤ) (c : ℕ) : ↑a = ↑b ↔ ↑c ∣ a-b


(which would be useful to have). Is there a reason why this is missing?

#### Michael Stoll (Mar 21 2022 at 19:26):

(Also, the naming of the results is not completely consistent; the last one has an additional _zmod...)

#### Alex J. Best (Mar 21 2022 at 20:18):

This is an ok place for the question, but #general or #Is there code for X? would also be ok for it.
I don't think there is any particular reason it is missing, most likely nobody needed precisely that lemma (or they just rewrote with docs#sub_eq_zero and used one of the ones you mentioned instead). Seems like a useful enough lemma to add to mathlib. Removing the zmod would also be welcome I'm sure

#### Michael Stoll (Mar 21 2022 at 20:35):

So how does this work? Do I wait and hope that somebody adds it eventually, or can/should I do it myself? In the latter case, I'll need some help, since I have never used github so far.
But probably this would be a good opportunity to learn how to do it, since I'll most likely want to add stuff to mathlib at some point.

#### Michael Stoll (Mar 21 2022 at 20:36):

I'm not sure about removing the _zmod, though, since I'd be afraid this could break code that uses the present name.

#### Alex J. Best (Mar 21 2022 at 20:40):

You can do it, this would be a nice first PR to mathlib I think, to get used to the workflow.
We have some instructions at https://leanprover-community.github.io/contribute/index.html, but the upshot is you can ask here for push access to the mathlib git repository (and give your github username). Then you push your updates to a branch of the leanprover-community/mathlib repo (using git) and create a PR for that branch (using the github website).

As for breaking existing code, we have continuous integration tools that will check that all of mathlib still builds with your changes, so that is fine (some things may need fixing as part of the PR but any breakage will be discovered). As for external projects there is potential for breakage when they update, but we try and smooth that by having tools to let people know about breaking changes, rather than by not making breaking changes, mathlib has very little in the way of backwards compatibility guarentees.

#### Michael Stoll (Mar 21 2022 at 20:42):

OK, thanks for the pointer! I'll have a look at how this works (but maybe not today...).

#### Eric Wieser (Mar 21 2022 at 23:06):

Does this lemma exist if you apply one of the first two lemmas you mention first?

#### Eric Wieser (Mar 21 2022 at 23:06):

maybe docs#int.dvd_sub?

#### Eric Wieser (Mar 21 2022 at 23:09):

a ≡ b [ZMOD c] ↔ c ∣ a-b


Is probably the lemma I would expect to have

#### Yaël Dillies (Mar 22 2022 at 00:00):

docs#int.modeq_iff_dvd

#### Michael Stoll (Mar 22 2022 at 09:31):

I think all these equivalences should be available.

#### Eric Wieser (Mar 22 2022 at 09:48):

Aren't you effectively stating that every lemma with a ≡ b [ZMOD c] on the LHS should have an analogous lemma about zmod?

#### Michael Stoll (Mar 22 2022 at 09:57):

Why not? The zmod version seems more useful to me, since zmod n is a finite ring (which allows for example the use of dec_trivial to prove statements [as I recently learned]).

#### Michael Stoll (Mar 22 2022 at 21:19):

Another question: How do I get

@[simp]
lemma zmod.coe_self_eq_zero (a : ℕ) : (a : zmod a) = 0 := by rw zmod.nat_coe_zmod_eq_zero_iff_dvd


to apply to (say) (2 : zmod 2)? The problem seems to be that 2 : zmod 2 is not the same as (2 : nat) : zmod 2.

#### Kyle Miller (Mar 22 2022 at 21:21):

Michael Stoll said:

(which allows for example the use of dec_trivial to prove statements [as I recently learned]).

In principle, dec_trivial can prove things about ZMOD too, and it might just be a matter of missing decidable instances.

#### Michael Stoll (Mar 22 2022 at 21:22):

Well, I guess it is good to have flexibility, so have both!

#### Kevin Buzzard (Mar 22 2022 at 21:27):

Michael Stoll said:

Another question: How do I get

@[simp]
lemma zmod.coe_self_eq_zero (a : ℕ) : (a : zmod a) = 0 := by rw zmod.nat_coe_zmod_eq_zero_iff_dvd


to apply to (say) (2 : zmod 2)? The problem seems to be that 2 : zmod 2 is not the same as (2 : nat) : zmod 2.

Yeah, good question. For numerals the way people usually do things is to prove results for bit0 and bit1. You can set_option pp.numerals false to see what Lean actually sees.

#### Michael Stoll (Mar 22 2022 at 21:29):

This kind of stumbling block is something I have repeatedly hurt my feet on. It would be nice if there were some kind of automatic coercion of numerals...

#### Kevin Buzzard (Mar 22 2022 at 21:29):

I think in Lean 4 they completely overhauled numerals.

#### Kyle Miller (Mar 22 2022 at 21:30):

Do tactic#norm_num or tactic#norm_cast work for you to normalize the numerals?

#### Michael Stoll (Mar 22 2022 at 21:31):

Instead of simp, I can do rw [(by norm_cast : (2 : zmod 2) = ((2 : ℕ) : zmod 2)), zmod.coe_self_eq_zero]. But I would rather want to have simp do that automatically.

#### Kyle Miller (Mar 22 2022 at 21:32):

Kevin Buzzard said:

I think in Lean 4 they completely overhauled numerals.

I'm probably misunderstanding it, but the mental model I have was that all numerals will be in "(2 : nat) : zmod 2" form

#### Michael Stoll (Mar 22 2022 at 21:32):

In that case, it should work, but it doesn't.

#### Kevin Buzzard (Mar 22 2022 at 21:37):

it should work in Lean 4 -- we're all using Lean 3

#### Kyle Miller (Mar 22 2022 at 21:42):

Regarding zmod.coe_self_eq_zero, I think that sort of lemma is more under the purview of norm_num. It can't normalize 2 : zmod 2 yet, but it's a matter of creating a norm_num tactic using code from norm_fin.

Here's a hack though:

meta def by_norm_cast : tactic unit := [norm_cast]

lemma zmod.coe_self_eq_zero (a : ℕ) (a' : zmod a) (h : a' = a . by_norm_cast) :
a' = 0 :=
begin
change a' = a at h,
rw [h, zmod.nat_coe_zmod_eq_zero_iff_dvd],
end

example : (2 : fin 2) = 0 :=
begin
rw zmod.coe_self_eq_zero 2 2,
end


#### Michael Stoll (Mar 22 2022 at 21:43):

Would this work as a simp lemma?

(deleted)

#### Michael Stoll (Mar 25 2022 at 16:54):

Coming back to the original topic, I would like to add this lemma (and change the names of two by removing "_zmod") to see how the process works. Can someone give me permission to push a branch? I'm MichaelStollBayreuth on Github. Thanks!

#### Bryan Gin-ge Chen (Mar 25 2022 at 16:57):

Michael Stoll said:

Coming back to the original topic, I would like to add this lemma (and change the names of two by removing "_zmod") to see how the process works. Can someone give me permission to push a branch? I'm MichaelStollBayreuth on Github. Thanks!

Thanks!

#### Michael Stoll (Mar 27 2022 at 14:45):

The PR is #12944. It is just the lemma with a one-line proof (after a suggestion by @Eric Wieser ).

#### Eric Wieser (Mar 27 2022 at 18:40):

Looks like 3 lines to me ;). You could use by rw ... instead of begin rw ... end next time to save two lines

#### Michael Stoll (Mar 27 2022 at 19:13):

What is the recommended style here, use begin ... end or by ... if it is a one-line proof?
by ...` for one-liners, not for twopliners