duplicate lemma?: dvd_add

Stream: general

[Stuart Presnell]

Why do we have these lemmas in data/nat/basic, rather than just having the iff versions that they depend upon?

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

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

[Yaël Dillies]

Those actually look better than the ones they are derived from, because their RHS are simpler than their LHS.

[Ruben Van de Velde]

Are the originals in core?

[Yaël Dillies]

Yep

[Kevin Buzzard]

These lemmas are useful -- you can rewrite with them. I used one of them in my ANTS talk two weeks ago in a live proof that there were infinitely many primes. I don't understand the question. What are "the iff versions"? The quoted lemmas are iff statements.

[Yaël Dillies]

Look at how they're proved!

[Kevin Buzzard]

Oh, so the answer is just "core is silly and we don't care enough to change it"

[Dean Young]

Hi Folks! I'm looking to start a project on categories here at the Lean community. I was wondering if anyone could help me out with finding a few of the basic constructions... maybe you know where to look.

I'd like to be able to:
1) Create a category given a type for the objects, morphisms, etc. (or some variation of this)
2) Create the opposite category
3) Product and internal hom of categories
4) Isomorphism classes of natural transformations.
5) Simplicial C w/ for a category C
6) Full subcategory consisting of objects matching a certain condition
7) Equalizer and coequilizer of functors.

[Kevin Buzzard]

[this has been asked again in a more appropriate thread https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Help.20finding.20some.20category.20definitions/near/296444530]