Andrew Yang

Results 78 comments of Andrew Yang

feat(Algebra/Category/Ring/Colimits): category of (possibly non-commutative ring) has colimits

If it is the same construction, can you show that `CommRingCat => RingCat` creates all colimits?

feat(Algebra/Category/Ring/Colimits): category of (possibly non-commutative ring) has colimits

Ah yes you are right. maintainer merge

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

good to go now.

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

!bench

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

!bench

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

I think this is the best I can do. @mattrobball any thoughts?

feat(AlgebraicGeometry/Limits): Spec preserves finite coproducts

1. There are two defs that aren't instant but the slowness seems to be spread evenly through tactics. 2. The file length is almost 2x So I think it's fine?

Adding a useful massing lemma: `not_mem_singleton_iff`

`git checkout master Mathlib/CategoryTheory/Grothendieck.lean` on that branch will reset the file to master. Be sure to back up first!

Adding a useful massing lemma: `not_mem_singleton_iff`

Yes.

Adding a useful massing lemma: `not_mem_singleton_iff`

Thanks! maintainer merge