int.sub_mod

Stream: Is there code for X?

[Scott Morrison]

I can't find

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

[Reid Barton]

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

[Shing Tak Lam]

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]

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

[Reid Barton]

Ah, well this was about a week ago

[Reid Barton]

and I was probably using an even older mathlib

[Shing Tak Lam]

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]

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]

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]

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]

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!