leanprover-community/mathlib

Pull Requests Commits

feat(meta/rb_map,tactic/monotonicity): replace rb_map.insert_cons (#1571)

robertylewis committed 6 years ago

b1654df1

feat(tactic/suggest): generalize and reimplement library_search (#1552)

Lucas Allen committed 6 years ago

74bed0c9

feat(algebra/big_operators): products and sums over `finset.Ico` (#1567)

urkud committed 6 years ago

f5446325

feat(tactic/lint): rename and refactor sanity_check (#1556)

robertylewis committed 6 years ago

173e70a0

feat(algebra/floor): prove `⌈x⌉ ≤ ⌊x⌋ + 1` (#1568)

urkud committed 6 years ago

ee398b66

chore(category_theory): using simps (#1500)

kim-em committed 6 years ago

05102ecb

feat(category_theory): def `is_isomorphic_setoid`, `groupoid.iso_equiv_hom` (#1506)

urkud committed 6 years ago

a1c0ad58

refactor(topology,calculus): change subset condition for composition (#1549)

sgouezel committed 6 years ago

e5fc2a70

docs(project): change example project [ci skip]

PatrickMassot committed 6 years ago

Verified cc19e30e

fix(topology/metric_space): fix uniform structure on Pi types (#1551)

sgouezel committed 6 years ago

905beb08

feat(ring_theory/algebraic): algebraic extensions, algebraic elements (#1519)

jcommelin committed 6 years ago

ee863ec1

archive(imo1988_q6): a formalization of Q6 on IMO1988 (#1455)

jcommelin committed 6 years ago

cbf81dff

feat(field_theory/finite): cardinality of images of polynomials (#1554)

ChrisHughes24 committed 6 years ago

ad8387cc

feat(data/zmod/basic): val_min_abs (#1548)

ChrisHughes24 committed 6 years ago

09fd631b

feat(data/polynomial): card_roots' (#1546)

ChrisHughes24 committed 6 years ago

c3d1bd71

fix(doc/contribute): fix broken link (#1547)

ChrisHughes24 committed 6 years ago

0ee1272a

docs(topology): some more module docstrings (#1544)

rwbarton committed 6 years ago

d716648f

feat(data/int/basic): int.nat_abs_eq_zero (#1545)

ChrisHughes24 committed 6 years ago

d10fd1e8

refactor(topology): mild reorganization (#1541)

rwbarton committed 6 years ago

646c035a

fix(topology/continuous_on): avoid duplicate instance arguments (#1542)

rwbarton committed 6 years ago

92a9a780

fix(topology/algebra/group_completion): remove redundant instance parameters (#1543)

rwbarton committed 6 years ago

995add3a

chore(docs/install/debian): Remove old sentence [ci skip]

PatrickMassot committed 6 years ago

Verified 76090bee

minor updates to the installation instructions (#1538)

abentkamp committed 6 years ago

27515619

refactor(ring_theory/algebra): alg_hom extends ring_hom and use curly brackets (#1529)

ChrisHughes24 committed 6 years ago

d5de8037

chore(algebra/ring): use curly brackets for ring_hom where possible (#1525)

ChrisHughes24 committed 6 years ago

6b7377aa

refactor(ring_theory/algebra): algebra should extend has_scalar not module (#1532)

ChrisHughes24 committed 6 years ago

38a0ffe9

fix(algebra/char_p): typo in docstring (#1537)

kbuzzard committed 6 years ago

338146b7

chore(algebra/group/hom): use curly brackets for instances where possible (#1524)

ChrisHughes24 committed 6 years ago

eb230d3b

chore(algebra/module): use curly brackets instead of square brackets in more places (#1523)

ChrisHughes24 committed 6 years ago

364c26e9

chore(linear_algebra): rename type variables (#1521)

abentkamp committed 6 years ago

43d3dee0

Newer Older