leanprover-community/mathlib3

Pull Requests Commits

chore(order/filter): rephrase filter.has_le (#1399)

PatrickMassot committed 6 years ago

7f208430

feat(bounded_lattice/has_lt): add a `lt` relation independent from `l… (#1366)

cipher1024 committed 6 years ago

28549094

feat(data/equiv/local_equiv): define local equivalences (#1359)

sgouezel committed 6 years ago

62928251

fix(tactic/norm_num): bugfix bad proof application (#1387)

digama0 committed 6 years ago

79a1f841

feat (logic/basic): exists_eq' (#1397)

ChrisHughes24 committed 6 years ago

3c224f0c

fix(topology/uniform_space): simplify continuity proof (#1396)

PatrickMassot committed 6 years ago

65ffb7b1

feat(order): add lemma (#1375)

fpvandoorn committed 6 years ago

06cffebf

feat(category_theory): finite products give a monoidal structure (#1340)

kim-em committed 6 years ago

5d59e8bd

feat(category_theory/sums): sums (disjoint unions) of categories (#1357)

kim-em committed 6 years ago

8cd16b97

feat(tactic/doc_blame): Use is_auto_generated (#1395)

PatrickMassot committed 6 years ago

b079298d

feat(measure_theory): prove that the Giry monad is a monad in the category_theory sense (#1259)

johoelzl committed 6 years ago

ff47fa31

chore(*): use localized command in mathlib (#1319)

fpvandoorn committed 6 years ago

b5b40c74

perf(data/gaussian_int): speed up div and mod (#1394)

ChrisHughes24 committed 6 years ago

4b6fcd90

chore(linear_algebra/determinant): simplify det_mul proof (#1392)

ChrisHughes24 committed 6 years ago

974d413b

feat(data/equiv/basic): add more functions for equivalences between complex types (#1384)

urkud committed 6 years ago

3a58b50f

feat(topology/uniform_space): Abstract completions (#1374)

PatrickMassot committed 6 years ago

a199f856

fix(restate_axiom): create lemmas from lemmas (#1390)

kim-em committed 6 years ago

c7d36292

feat(data/fintype): prove `card (subtype p) ≤ card α` (#1383)

urkud committed 6 years ago

94205c46

feat(category_theory): define `iso.conj` and friends (#1381)

urkud committed 6 years ago

227b6821

feat(category_theory/limits): construct limits from products and equalizers (#1362)

kim-em committed 6 years ago

57d4b411

chore(data/nat/gcd): remove pointless parentheses (#1386)

khoek committed 6 years ago

fe7695ba

feat(data/nat/gcd): add simple lemmas (#1382)

urkud committed 6 years ago

d35dc135

chore(category_theory/notation): consistently use notation for functor.id (#1378)

kim-em committed 6 years ago

6d2b3ed8

feat(data/option/basic): eq_some_iff_get_eq (#1370)

ChrisHughes24 committed 6 years ago

df65dde5

feat(category_theory/limits/of_nat_iso): missing parts of the limits API (#1355)

kim-em committed 6 years ago

72ce940c

chore(unicode): improve arrows (#1373)

khoek committed 6 years ago

455f0603

doc(contribute): add detailed instructions for cache-olean [skip ci] (#1367)

fpvandoorn committed 6 years ago

4c5c4dc7

feat(sanity_check): improve sanity_check (#1369)

fpvandoorn committed 6 years ago

2db7fa45

feat(category_theory/limits): special shapes (#1339)

kim-em committed 6 years ago

afe51c76

Fix `tactic.exact` timeout in `apply'` (#1371)

Zhouhang Zhou committed 6 years ago

1278efd6

Newer Older