leanprover-community/mathlib

Pull Requests Commits

compare definitions of projective

kim-em committed 4 years ago

3976df4a

kim-em committed 4 years ago

4eb80113

Merge branch 'homology_redesign' into projective_refactor

kim-em committed 4 years ago

67af1205

Merge branch 'subobject_limits' into homology_redesign

kim-em committed 4 years ago

4932b5c8

Merge branch 'zero' into homology_redesign

kim-em committed 4 years ago

52f82acc

removing a simps that was unnecessary, and resulting in a linter timeout

kim-em committed 4 years ago

139c457c

Merge branch 'zero' of github.com:leanprover-community/mathlib into zero

kim-em committed 4 years ago

c7d83b70

kim-em committed 4 years ago

121b4d62

Apply suggestions from code review

kim-em committed 4 years ago

Verified 683ac43a

feat(category_theory/*/projective): refactor treatment of projective objects

kim-em committed 4 years ago

f2be42db

kim-em committed 4 years ago

bc59d448

feat(algebra/homology): redesign of homological complexes

kim-em committed 4 years ago

b9c853b1

Merge branch 'zero' into homology_redesign

kim-em committed 4 years ago

a4635dc5

Merge branch 'mono_of_kernel_iso_zero' into homology_redesign

kim-em committed 4 years ago

723796d9

Merge branch 'subobject_limits' into homology_redesign

kim-em committed 4 years ago

01f2cc4a

Merge branch 'subobject2' into subobject_limits

kim-em committed 4 years ago

79e72a0d

Merge branch 'subobject_limits' into homology_redesign

kim-em committed 4 years ago

292109b1

kim-em committed 4 years ago

3caf09d2

feat(category_theory/subobjects): more about kernel and image subobjects

kim-em committed 4 years ago

d6169aaf

Merge branch 'subobject2' into subobject_limits

kim-em committed 4 years ago

62850b81

feat(category_theory/subobject): minor tweaks

kim-em committed 4 years ago

6fa9bfeb

feat(category_theory/preadditive): reformulation of mono_of_kernel_zero

kim-em committed 4 years ago

25a68273

add simp lemmas

kim-em committed 4 years ago

dc8ac574

feat(category_theory/.../zero): if a zero morphism is a mono, the source is zero

kim-em committed 4 years ago

2ab67aa2

feat(category_theory/.../images): image.pre_comp_epi_of_epi

kim-em committed 4 years ago

ce8b14e5

feat(data/finset/lattice): add sup_image (#7428)

eric-wieser committed 4 years ago

5a91d05e

feat(ring_theory/finiteness): add lemmas (#7409)

riccardobrasca committed 4 years ago

37735250

chore(data/fintype): rework `fintype.equiv_fin` and dependencies (#7136)

Vierkantor committed 4 years ago

67dad976

chore(*): update to lean 3.30.0c (#7264)

gebner committed 4 years ago

048240e8

feat(category_theory/preadditive): Schur's lemma (#7366)

kim-em committed 4 years ago

7da83031

Older