leanprover-community/mathlib3

Pull Requests Commits

restoring abstract stuff

kim-em committed 5 years ago

3f74a06d

removing abstract enriched categories; into branch enriched_abstract

kim-em committed 5 years ago

bc36a65c

kim-em committed 5 years ago

7a3a2880

kim-em committed 5 years ago

caa8f1db

feat(algebra): the forgetful functor Module ℤ ⥤ Ab is an equivalence (#2130)

kim-em committed 5 years ago

Verified e6ccfe03

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

d313d14e

feat(algebra/category/Group): the free-forgetful adjunction for AddCommGroup (#2141)

kim-em committed 5 years ago

Verified 559921a5

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

465f5996

feat(algebra): monoidal category of R-modules (#2125)

kim-em committed 5 years ago

Verified 81d3ebf3

refactor(ring_theory/subring): use bundled homs (#2144)

urkud committed 5 years ago

Verified 3d621b5e

feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) (#2139)

TwoFX committed 5 years ago

Verified ade1ee30

kim-em committed 5 years ago

45d6f28c

kim-em committed 5 years ago

8e0281f7

chore(algebra/category/CommRing/limits): avoid `is_ring_hom` (#2142)

urkud committed 5 years ago

Verified 49f5fb88

chore(linear_algebra/basic): simplify two proofs (#2123)

urkud committed 5 years ago

Verified 32c2768b

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

aec62dc4

refactor(*): migrate some files to bundled ring homs (#2133)

urkud committed 5 years ago

Verified b54960d1

chore(algebra/field*, field_theory/subfield): drop some `x ≠ 0`, use `division_ring` (#2136)

urkud committed 5 years ago

Verified 1c449b6c

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

5fe72b6b

doc(*): switch from update-mathlib to leanproject (#2093)

gebner committed 5 years ago

Verified f5787f53

kim-em committed 5 years ago

66c19e09

kim-em committed 5 years ago

dd554353

feat(category_theory/opposites): add nat_iso.unop (#2132)

thjread committed 5 years ago

Verified 81311088

Fix a typo (#2137)

TwoFX committed 5 years ago

Verified 7d357d74

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

35a6e682

feat(topology): is_closed_proj_of_compact (#2069)

PatrickMassot committed 5 years ago

Verified 1b0a7493

Merge branch 'monoidal_Module' into enriched

kim-em committed 5 years ago

874d6571

reduce use of @

kim-em committed 5 years ago

9691c2fe

feat(category_theory/limits): construct equalizers from pullbacks and products (#2124)

b-mehta committed 5 years ago

Verified 7c8dc2ad

chore(category_theory/cones): make functor argument of forget explicit (#2128)

kim-em committed 5 years ago

Verified 7cffe252

Older