leanprover-community/mathlib

Pull Requests Commits

fix(category_theory/limits): require explicit instances of has_zero_morphisms (#2169)

TwoFX committed 6 years ago

Verified 6af37d37

fix(scripts/mk_nolint): fix error introduced by #2090 (#2170)

robertylewis committed 6 years ago

Verified 422f6400

feat(lint): run some linters on automatically generated declarations (#2090)

fpvandoorn committed 6 years ago

Verified e94fef01

feat(data/real/*nnreal): add division lemmas (#2167)

sgouezel committed 6 years ago

Verified 496939ce

feat(category_theory): split epis and monos, and a result about (co)projections (#2146)

kim-em committed 6 years ago

Verified 4754368c

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

bc087d82

chore(order/liminf_limsup): lint and cleanup the file (#2162)

sgouezel committed 6 years ago

Verified 7a5496f6

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

007b575c

feat(tactic): command for adding tactic, command, and attribute documentation (#2114)

robertylewis committed 6 years ago

Verified 42b92aaa

doc(docs/install/windows): emphasize projects link (#2150)

kbuzzard committed 6 years ago

Verified 04c73819

feat(category_theory/image): comparison maps for precomposition (#2153)

kim-em committed 6 years ago

Verified 555528e1

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

1e38cb1b

feat(category_theory/monad/limits): forgetful creates colimits (#2138)

b-mehta committed 6 years ago

Verified ff84bf47

feat(analysis/normed_space/operator_norm): completeness of the space of operators (#2160)

sgouezel committed 6 years ago

Verified 4aed8625

feat(category_theory/limits): Convenience methods for building limit (co)forks (#2155)

TwoFX committed 6 years ago

Verified d8e5d99a

feat(category_theory/limits): pullbacks from binary products and equalizers (#2143)

TwoFX committed 6 years ago

Verified c240fcb3

feat(category_theory/limits): kernel forks (#2156)

TwoFX committed 6 years ago

Verified fbe2ce09

chore(nnreal): replace coe_le with coe_le_coe (#2159)

sgouezel committed 6 years ago

Verified 87f8ab22

chore(field_theory/finite): spelling mistake (#2157)

ChrisHughes24 committed 6 years ago

Verified 7104132e

refactor(logic/function): inv_fun takes a nonempty instance instead of inhabited (#2148)

ChrisHughes24 committed 6 years ago

Verified 0cbfbabb

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

b314df2e

feat(category_theory): comonads and coalgebras (#2134)

b-mehta committed 6 years ago

Verified 8c2a254c

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

e4bf0bfa

feat(category_theory): limits and colimits in Ab (#2097)

kim-em committed 6 years ago

Verified 54339730

doc(docs/install/*): emphasize projects link (#2151)

kbuzzard committed 6 years ago

Verified 2e781eb0

feat(category_theory/comma): some limits in the over category and iterated slices (#2131)

b-mehta committed 6 years ago

Verified 2065438d

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

cc39a150

refactor(data/equiv/algebra): split (#2147)

urkud committed 6 years ago

Verified 7b2be40f

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

kim-em committed 6 years ago

Verified e6ccfe03

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

d313d14e

Older