leanprover-community/mathlib

Pull Requests Commits

kim-em committed 6 years ago

105a151d

chore(category_theory): change monoidal_of_has_finite_products to use binary products

kim-em committed 6 years ago

ab9b80e0

kim-em committed 6 years ago

2d816a8e

kim-em committed 6 years ago

44e44d2d

feat(category_theory): some natural isomorphisms related to composition by functors

kim-em committed 6 years ago

4ec867f4

chore(category_theory): missing simp lemmas

kim-em committed 6 years ago

b89fec00

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

b3ef6859

Merge remote-tracking branch 'origin/master' into enriched

kim-em committed 6 years ago

413413f5

associator_hom done

kbuzzard committed 6 years ago

5cfa7766

refactor(*): drop `lattice` namespace (#2166)

urkud committed 6 years ago

Verified 9dbc6069

chore(category_theory/images): fix some minor problems (#2182)

kim-em committed 6 years ago

Verified a20f378f

feat(category_theory): regular monos (#2154)

kim-em committed 6 years ago

Verified 4bc32ae4

chore(category_theory/isomorphism): use @[simps] (#2181)

kim-em committed 6 years ago

Verified 445e3320

kim-em committed 6 years ago

d2d8cf2e

chore(category_theory/binary_products): tweak spacing in notation (#2184)

kim-em committed 6 years ago

Verified e2b0e387

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

034685b9

two proofs of right_unitor_hom

kbuzzard committed 6 years ago

5c809d0e

feat(topology/algebra/infinite_sum): dot notation, cauchy sequences (#2171)

sgouezel committed 6 years ago

Verified 00d9f1de

chore(*): switch to lean 3.7.1c (#2106)

gebner committed 6 years ago

Verified e719f8ee

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

69f7bf86

feat(topology/bounded_continuous_functions): more general uniform convergence (#2165)

sgouezel committed 6 years ago

Verified 5f62d3bb

feat(analysis/complex/exponential): real powers of nnreals (#2164)

sgouezel committed 6 years ago

Verified 739e831f

feat(category_theory): images in Ab and Type (#2101)

kim-em committed 6 years ago

Verified f07a1ebf

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

ooh, almost there

kim-em committed 6 years ago

59e93168

kim-em committed 6 years ago

421eaefa

kim-em committed 6 years ago

070645b7

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

Newer Older