## Stream: general

#### Stuart Presnell (Aug 23 2022 at 13:34):

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 :=

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


#### Yaël Dillies (Aug 23 2022 at 13:40):

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

#### Ruben Van de Velde (Aug 23 2022 at 13:45):

Are the originals in core?

Yep

#### Kevin Buzzard (Aug 24 2022 at 06:09):

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 (Aug 24 2022 at 06:10):

Look at how they're proved!

#### Kevin Buzzard (Aug 24 2022 at 06:11):

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

#### Dean Young (Aug 31 2022 at 20:25):

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.