Explicit theorem about div/mod injectivity.

Stream: Is there code for X?

[Wrenna Robson]

I sort of can't believe we don't have the following, but I haven't yet found it:

theorem mod_div_inj {a b n : Nat} :
a = b ↔ a % n = b % n ∧ a / n = b / n := by grind [Nat.div_add_mod]

It is implicit in, for instance, Nat.divModEquiv, though only for NeZero n. But it feels like a more fundamental theorem - I was expecting to find it in Core, even.

[Bbbbbbbbba]

I guess it is deemed a little too trivial with Nat.div_add_mod?

[Wrenna Robson]

Well yes that's kind of what you use, but in practice it's useful to have the above.

[Yury G. Kudryashov]

I think it makes sense to have this, both as iff and as a % n = b % n → a / n = b / n → a = b.

[Wrenna Robson]

Yes agreed.

[Wrenna Robson]

You might want to make n explicit rather than implicit as pretty much in many applications of it it may not be natural.

[Wrenna Robson]

Also I think this is also true in Int to at least some degree? Not sure if it's wanted there but you can see the use. The lack of any hypothesis on n (it can be zero!) is IMO particularly nice.

[Jakub Nowak]

Yury G. Kudryashov said:

I think it makes sense to have this, both as iff and as a % n = b % n → a / n = b / n → a = b.

Why do you want implication too?

[Wrenna Robson]

More convenient for apply I assume

[Jakub Nowak]

I know what you mean, but it's just the same thing under different name (instead of mod_div_inj.mpr). There's no change in convenience of person who writes the proof. There might be some for someone who reads. But I would say it's a negative convenience to have two different names for the same thing.

[Wrenna Robson]

Well we do this kind of thing all the time! It's like ext versus ext_iff.

[Jakub Nowak]

Ah, wait, no, it's different than mod_div_inj.mpr. It unbundles And with apply.

[Wrenna Robson]

Yes.

[Wrenna Robson]

Like in terms of good-mannered API, I think you want both.

[Jakub Nowak]

Sure, but I think it only makes sense in the case like here, where one side has either forall or And.

[Wrenna Robson]

Sure, not all iff should have it.

[Wrenna Robson]

@Yury G. Kudryashov Should this be in core, Batteries or Mathlib? I could PR it into the latter for now and worry about upstreaming later?

[Yury G. Kudryashov]

I think that it makes sense to PR it to Mathlib, then it will (or will not) get upstreamed later.

[Wrenna Robson]

Where should it go in Mathlib nowadays? We seem to not have any of the % theorems there anymore as they've all been upstreamed.

[Wrenna Robson]

Probably just Basic.

[Markus Himmel]

There is Mathlib.Data.Nat.Init for results that explicitly do not depend on anything in mathlib. The standard library team looks at these Init files semi-regularly for things to upstream.

[Wrenna Robson]

Ah, thank you!

[Wrenna Robson]

Do we use theorem or lemma nowadays? I've got out of the habit of using the latter but I can't recall what the style is.

[Ruben Van de Velde]

For results (somewhat) likely to move to the standard library eventually, I'd use theorem, but there's not really a strong policy right now

[Wrenna Robson]

Thanks.

[Wrenna Robson]

#34201

[Kim Morrison]

I took the liberty of then moving some of these theorems up to lean4. Thank you for writing them! #12258

[Wrenna Robson]

lean4#12258

[Wrenna Robson]

Brill! Thanks for considering them.