[Merged by Bors] - feat(data/nat/basic): (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n

[adomani]

... and the dual statement
(∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/semilattice.2C.20dvd.2C.20associated

Co-authored-by: tb65536 tb65536@users.noreply.github.com

---

[Julian-Kuelshammer]

... and the dual statement
(∀ a : ℕ, a ∣ m ↔ a ∣ n) ↔ m = n

Zulip discussion:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members

Co-authored-by: Julian-Kuelshammer 68201724+Julian-Kuelshammer@users.noreply.github.com

If you want to list a coauthor, it should be @tb65536 in #6876, not me.

[adomani]

If you want to list a coauthor, it should be @tb65536 in #6876, not me.

Julian, thanks for the correction: I updated the description!

[awainverse]

It should be possible to prove this for any comm_cancel_monoid_with_zero M with unique (units M), which are instances nat already has. In algebra/associated, you can find associated_iff_eq and dvd_dvd_iff_associated, which you can string together in that context.

[adomani]

@awainverse Yes, there was an extensive discussion about this in the Zulip chat, but the link changed name: I will change it above, but here it is for the moment:
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/semilattice.2C.20dvd.2C.20associated

[Vierkantor]

Thanks!

bors r+

[bors]

Build failed (retrying...):

• Run tests

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests