leanprover-community/mathlib

Pull Requests Commits

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

Unknown committed 6 years ago

5a1731f6

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

feat(topology/sequences): every first-countable space is sequential (#1528)

gebner committed 6 years ago

dc788a0b

chore(ring_theory/adjoin_root): remove some unused decidable_eq (#1530)

ChrisHughes24 committed 6 years ago

7d792ec4

fix(tactic/{use,ring}): instantiate metavariables in goal (#1520)

robertylewis committed 6 years ago

a17a9a6a

refactor(topology/algebra/polynomial): move topology.instances.polynomial (#1527)

rwbarton committed 6 years ago

45633aa0

docs(data/holor): some additional documentation (#1526)

rwbarton committed 6 years ago

0ea83c09

feat(algebra/ordered...): Two tiny lemmas (#1522)

PatrickMassot committed 6 years ago

6ccfe5a3

Newer Older