leanprover-community/mathlib

Pull Requests Commits

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

doc(linear_algebra/basis): add doc (#1503)

abentkamp committed 6 years ago

7c560512

chore(analysis): put lemmas in normed_field namespace (#1517)

PatrickMassot committed 6 years ago

6b15eb29

refactor(topology/continuous_on): move continuous_{on,within_at} to own file (#1516)

rwbarton committed 6 years ago

afda1a2c

feat(tactic/find): find defs as well as theorems (#1512)

robertylewis committed 6 years ago

045d931e

feat(data/quot): define `quotient.map₂'`, use it for group quotient (#1507)

urkud committed 6 years ago

ef7248f7

chore(topology/algebra/group_completion): missing namespace (#1518)

PatrickMassot committed 6 years ago

bf224080

refactor(topology/dense_embedding): move dense embeddings to new file (#1515)

rwbarton committed 6 years ago

1bf831f2

doc(topology/order): module and definition docstrings (#1505)

rwbarton committed 6 years ago

b3eb34d2

refactor(topology/list): move topology of lists, vectors to new file (#1514)

rwbarton committed 6 years ago

f519a125

refactor(topology/maps): avoid repetition in dense embeddings (#1513)

rwbarton committed 6 years ago

ddbeb7eb

feat(group_theory/submonoid): define `subtype.comm_monoid` (#1511)

urkud committed 6 years ago

78a78efc

chore(topology): sanity_check pass (#1510)

PatrickMassot committed 6 years ago

7df0e350

feat(algebra/opposites): add some trivial `@[simp]` lemmas (#1508)

urkud committed 6 years ago

98dbe27a

fix(data/list/min_max): docs typo (#1504)

minchaowu committed 6 years ago

2f1bd1e5

feat(algebra/Module): the category of R-modules (#1420)

rspencer01 committed 6 years ago

343237d1

feat(algebra): commuting elements (#1089)

NeilStrickland committed 6 years ago

494132e1

doc(linear_algebra/basic): add module and declaration doc strings (#1501)

robertylewis committed 6 years ago

3c58f160

feat(tactic/squeeze_simp): better handling of private declarations (#1498)

cipher1024 committed 6 years ago

f8543711

chore(*): fix errors in library and sanity_check (#1499)

fpvandoorn committed 6 years ago

4ca1e634

feat(data/equiv/algebra): automorphism groups for other structures (#1141)

callum-sutton committed 6 years ago

4bb8d447

fix(dioph): remove global vector3 notation (#1502)

fpvandoorn committed 6 years ago

bea1c20d

chore(.): delete CODEOWNERS

robertylewis committed 6 years ago

39ca4f14

feat(tactic/delta_instance): handle parameters and use in library (#1483)

robertylewis committed 6 years ago

5ed5f594

chore(linear_map): use curly brackets for type class in linear_map coe_to_fun (#1493)

ChrisHughes24 committed 6 years ago

800dba4f

Newer Older