leanprover-community/mathlib3

Pull Requests Commits

kim-em committed 5 years ago

f3f20b8f

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

af0cf30e

refactor(scripts/mk_nolint): produce nolints.txt file during linting (#2194)

gebner committed 5 years ago

Verified 0bd8b94d

doc(docs/contribute/index.md): remove obsolete recommendation to use lean-3.7.2 branch (#2206)

gebner committed 5 years ago

Verified dd85db0c

chore(leanpkg.toml): Lean 3.7.2c (#2203)

bryangingechen committed 5 years ago

Verified bc84a205

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

kim-em committed 5 years ago

Verified 34bac8d3

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

kim-em committed 5 years ago

Verified 99ba8f44

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

kim-em committed 5 years ago

Verified 94201677

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

b224943d

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

kim-em committed 5 years ago

Verified 8d44098d

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

kim-em committed 5 years ago

Verified 0f1b4654

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

kim-em committed 5 years ago

Verified c66c4afa

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

kim-em committed 5 years ago

Verified d93e0ddb

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

kim-em committed 5 years ago

Verified b4e6313a

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

cc041325

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

kim-em committed 5 years ago

Verified 6c97ce02

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

ChrisHughes24 committed 5 years ago

Verified d12bbc00

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

3dd95a2e

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

kim-em committed 5 years ago

Verified 1a398a72

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

sgouezel committed 5 years ago

Verified 344a41e8

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

b3ef6859

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

urkud committed 5 years ago

Verified 9dbc6069

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

kim-em committed 5 years ago

Verified a20f378f

feat(category_theory): regular monos (#2154)

kim-em committed 5 years ago

Verified 4bc32ae4

kim-em committed 5 years ago

5d43fb26

Merge branch 'regular_mono' into coequalizer_kernel_pair

kim-em committed 5 years ago

f1d1a9b0

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

kim-em committed 5 years ago

Verified 445e3320

kim-em committed 5 years ago

9aae21ae

kim-em committed 5 years ago

0398cfb7

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

kim-em committed 5 years ago

Verified e2b0e387

Older