leanprover-community/mathlib

Pull Requests Commits

doc(contribute/bors.md): update some outdated info (#3209)

bryangingechen committed 5 years ago

da210bf9

feat(nat, lattice): preliminaries for Haar measure (#3190)

fpvandoorn committed 5 years ago

2f6a5f59

feat(algebra/big_operators): add induction principles (#3197)

jalex-stark committed 5 years ago

4e2b46a7

feat(subtype): standardize (#3204)

fpvandoorn committed 5 years ago

a220286a

chore(scripts): update nolints.txt (#3206)

leanprover-community-bot committed 5 years ago

dd2f1b96

feat(category_theory/cones): cone functoriality is fully faithful (#3202)

b-mehta committed 5 years ago

247fe80d

chore(tactic/linarith): remove final linting error (#3196)

robertylewis committed 5 years ago

adcd09d1

feat(set): preliminaries for Haar measure (#3189)

fpvandoorn committed 5 years ago

e7e9f30c

feat(analysis/normed_space/real_inner_product): sums and bilinear form (#3187)

jsm28 committed 5 years ago

8413b3f4

feat(category_theory/limits): limit of point iso (#3188)

b-mehta committed 5 years ago

6ed3325a

chore(scripts): update nolints.txt (#3192)

leanprover-community-bot committed 5 years ago

c6fd69d3

chore(category_theory/pempty): use discrete pempty instead of a special pempty category (#3191)

b-mehta committed 5 years ago

78d67807

feat(data/set/basic): +2 lemmas, +2 `simp` attrs (#3182)

urkud committed 5 years ago

2d270ff1

chore(*): last preparations for Heine (#3179)

PatrickMassot committed 5 years ago

ef62d1c0

feat(algebra/big_operators): telescoping sums (#3184)

jalex-stark committed 5 years ago

6624509e

feat(ring_theory/matrix_equiv_tensor): matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R) (#3177)

kim-em committed 5 years ago

5b97da63

chore(category/*): linting (#3178)

kim-em committed 5 years ago

3cfc0e73

feat(data/fintype): trunc_sigma_of_exists (#3166)

kim-em committed 5 years ago

c3923e39

chore(category_theory/equivalence) explicit transitivity transformation (#3176)

b-mehta committed 5 years ago

616cb5e6

chore(scripts): update nolints.txt (#3174)

leanprover-community-bot committed 5 years ago

abae5a3c

feat(tactic/abel) teach abel to gsmul_zero (#3173)

alexjbest committed 5 years ago

43a2b24d

refactor(ring_theory/ideals): make local_ring a prop class (#3171)

kbuzzard committed 5 years ago

db7a53af

feat(category/default): comp_dite (#3163)

kim-em committed 5 years ago

afc1c24e

feat(category_theory/limits): isos from reindexing limits (#3100)

kim-em committed 5 years ago

c6f629bc

feat(*): bump to Lean 3.16.5 (#3170)

kim-em committed 5 years ago

158e84ae

chore(*): assorted lemmas about `set` and `finset` (#3158)

urkud committed 5 years ago

7d331eb9

feat(category_theory): show a pullback of a regular mono is regular (#2780)

b-mehta committed 5 years ago

80a08778

feat(filter, topology): cluster_pt and principal notation, redefine compactness (#3160)

PatrickMassot committed 5 years ago

3f868fab

feat(category/adjunction): missing simp lemmas (#3168)

kim-em committed 5 years ago

e7db701e

chore(category/discrete): missing simp lemmas (#3165)

kim-em committed 5 years ago

d86f1c83

Newer Older