leanprover-community/mathlib

Pull Requests Commits

feat(category_theory): add naturality_assoc simp lemma (#2200)

kim-em committed 6 years ago

Verified 34bac8d3

chore(category_theory): change monoidal_of_has_finite_products to use binary products (#2190)

kim-em committed 6 years ago

Verified 99ba8f44

feat(category_theory): unbundled functors and lax monoidal functors (#2193)

kim-em committed 6 years ago

Verified 94201677

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

b224943d

feat(finsupp): move convolution product to type wrapper `add_monoid_algebra`. (#2135)

kim-em committed 6 years ago

Verified 8d44098d

feat(category_theory/limits): the isomorphism expressing preservation of chosen limits (#2192)

kim-em committed 6 years ago

Verified 0f1b4654

chore(algebra/Module/monoidal): add the simp lemmas for unitors and associativity (#2196)

kim-em committed 6 years ago

Verified c66c4afa

chore(category_theory): missing simp lemmas (#2188)

kim-em committed 6 years ago

Verified d93e0ddb

feat(category_theory): subsingleton (has_zero_morphisms) (#2180)

kim-em committed 6 years ago

Verified b4e6313a

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

cc041325

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

kim-em committed 6 years ago

Verified 6c97ce02

feat(data/zmod): lemmas about totient and zmod (#2158)

ChrisHughes24 committed 6 years ago

Verified d12bbc00

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

3dd95a2e

docs(category_theory/limits): adding many docstrings (#2185)

kim-em committed 6 years ago

Verified 1a398a72

feat(data/finset): monotone bijection from fin k (#2163)

sgouezel committed 6 years ago

Verified 344a41e8

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

b3ef6859

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

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

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

Older