adding two lemmas about division

[semorrison]

These are very minor lemmas, and I don't know how they should be named, but I think they should be in.

These came up when I was trying to record a video demonstrating proving the infinitude of primes in Lean. (Essentially following the mathlib proof.)

It comes to the step where you know p | fact N and p | fact N + 1, and you're trying to deduce p | 1. Without magically knowing that the relevant lemma is nat.dvd_add_iff_right in core, I challenge you to explain to somehow to find that lemma!

If we add these two lemmas, at least one can do the obvious thing:

#find _ ∣ _ → _ ∣ _ → _ ∣ _

[digama0]

The idea is that this is a simplification of the second hypothesis. In fact you could make it a biconditional with the other hypothesis instead, resulting in the slightly peculiar d | m + n -> (d | m <-> d | n), but I like to think of dvd_add_iff_left as an inversion of dvd_add with one of its hypotheses. (As a general rule, if it can be biconditional it will be, in mathlib.)

[johoelzl]

I'm fine with adding a biconditional in the opposite direction.

[digama0]

Which do you mean? I think that it is better for d | m + n to be the LHS of a biconditional, because it is the more complex side so it is in line with our general principles for simp-like lemmas. For the backward biconditional I quoted I guess it could be either way, although it makes sense to keep m on the left since it was on the left to start with.

[johoelzl]

I mean nat.dvd_add_iff_left and nat.dvd_add_iff_left. These are their current forms:

theorem dvd_add_iff_left {a b c : α} (h : a ∣ c) : a ∣ b ↔ a ∣ b + c
theorem dvd_add_iff_right {a b c : α} (h : a ∣ b) : a ∣ c ↔ a ∣ b + c

And I also think the + should be on the LHS instead of the RHS.

[digama0]

Oh yes, I agree with you there.

[semorrison]

Okay, I think this is saying we want lemmas

theorem XXX {a b c : α} (h : a ∣ c) : a ∣ b +c ↔ a ∣ b
theorem YYY {a b c : α} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c

Unfortunately I don't understand the naming scheme well enough to name these. If someone wants to tell me one of the names, I can revise this PR.

[digama0]

They should be dvd_add_iff_left/right just as in Johannes's comment.

[semorrison]

But -- that's what they are already called in core. I thought we would need new names?!

[digama0]

I don't think the core theorems require modification, the remark above is about the nat versions, which are in mathlib, I think

[semorrison]

No, nothing is in mathlib. We have

protected theorem dvd_add_iff_right {k m n : ℕ} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n := ...
protected theorem dvd_add_iff_left {k m n : ℕ} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n := ...

in library/init/data/nat/lemmas.lean, and

  theorem dvd_add_iff_left {a b c : α} (h : a ∣ c) : a ∣ b ↔ a ∣ b + c := ...
  theorem dvd_add_iff_right {a b c : α} (h : a ∣ b) : a ∣ c ↔ a ∣ b + c := ...

in library/init/algebra/ring.lean.

This leaves me pretty confused about what you and Johannes are suggesting! I guess my best guess is we should have

  theorem dvd_iff_add_right {a b c : α} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b := ...
  theorem dvd_iff_add_left {a b c : α} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c := ...

for both [ring α] and for nat.

I'm not particularly confident I have my left and right correct here, nor that we really ought to change anything...