Zulip Chat Archive

Stream: Is there code for X?

Topic: int.sub_mod


Scott Morrison (May 22 2020 at 09:30):

I can't find

lemma int.sub_mod (a b n : ) : (a - b) % n = ((a % n) - (b % n)) % n := ...

Reid Barton (May 22 2020 at 09:40):

I couldn't find the add version either (for nat)

Shing Tak Lam (May 22 2020 at 09:41):

Reid Barton said:

I couldn't find the add version either (for nat)

I thought I PR-ed that recently? I PR-ed some other lemmas and golfed the proof of that one. The lemma was added in #2522

Reid Barton (May 22 2020 at 09:41):

or technically I did find it, but only as the first line of the proof of a lemma

Reid Barton (May 22 2020 at 09:41):

Ah, well this was about a week ago

Reid Barton (May 22 2020 at 09:42):

and I was probably using an even older mathlib

Shing Tak Lam (May 22 2020 at 09:43):

But I don't think the lemma that Scott posted is in mathlib at all, at least when I went through mathlib to port nat and int lemmas to eachother I did see anything like it.

Scott Morrison (May 22 2020 at 10:52):

Thanks, Reid and Shing. I've refactorede what I'm working on to use less % and more zmod in the meantime, so I'm not going to do these lemmas today.

Scott Morrison (May 22 2020 at 10:53):

It does look like there's a fair bit missing here. I can't find nat.pow_mod or int.pow_mod, either.

Patrick Massot (May 22 2020 at 10:58):

Scott, if you are doing modular arithmetic those days then don't hesitate to adopt my attempt at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/even.20or.20odd/near/195632609

Scott Morrison (May 22 2020 at 11:03):

Fortunately today's project doesn't require any case splitting like this. You should PR that tactic, or at least make an issue describing what it should do!


Last updated: Dec 20 2023 at 11:08 UTC