leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into back

khoek committed 6 years ago

Verified dac95de6

refactor(linear_algebra/basic): use smul_right (#1640)

sgouezel committed 6 years ago

9af7e5b5

feat(lint): add priority test for instances that always apply (#1625)

fpvandoorn committed 6 years ago

1710fd8b

fix(tactic/elide): was untested and buggy. Fixed a few issues (#1638)

cipher1024 committed 6 years ago

5f17abcc

chore(category_theory/whiskering): clean up (#1613)

kim-em committed 6 years ago

df916232

chore(data/set/finite): move defns up hierarchy; rename fintype_of_finset, card_fintype_of_finset (#1615)

kim-em committed 6 years ago

cd0bc32b

feat(order/conditionally_complete_lattice): add complete_linear_order instance for enat (#1633)

gebner committed 6 years ago

6b51787e

feat(tactic/simps): allow let-expressions (#1626)

fpvandoorn committed 6 years ago

780cbc98

feat(.travis.yml): add linting to test stage (#1606)

robertylewis committed 6 years ago

d43f7f9c

feat(data/fintype): fintype.card_subtype_lt (#1635)

ChrisHughes24 committed 6 years ago

aadfde68

feat(number_theory/sum_four_squares): every natural number is the sum of four square numbers (#1560)

ChrisHughes24 committed 6 years ago

ca900815

chore(category_theory): speed-up monoidal.of_has_finite_products (#1616)

kim-em committed 6 years ago

6030ff0a

cleanup(order|string) (#1629)

fpvandoorn committed 6 years ago

e6e25d06

feat(rat): give Q-algebra structure on field (#1628)

fpvandoorn committed 6 years ago

b9e3dbba

fix(*): use has_coe_t (#1627)

fpvandoorn committed 6 years ago

b5b674c2

feat(tactic/rcases): transport the `cases h : e` syntax to `rcases` (#1611)

cipher1024 committed 6 years ago

0ea3dfe4

feat(tactic/lint): silent linting (#1580)

robertylewis committed 6 years ago

7a8f53e1

chore(ring_theory/algebra): add docstring to algebra.comap and remove unused instances (#1624)

ChrisHughes24 committed 6 years ago

94e368c5

fix(tactic/omega): fix omega bugs, add docstring (closes #1484) (#1620)

skbaek committed 6 years ago

c2e81ddd

feat(linear_algebra/basic): define algebra structure on endomorphisms of module (#1618)

Oliver Nash committed 6 years ago

1fa03c29

fix(data/mv_polynomial): generalize equivs to comm_semiring (#1621)

rwbarton committed 6 years ago

89ece147

chore(category_theory): remove superfluous lemma (#1614)

kim-em committed 6 years ago

8a45d98f

feat(linear_algebra/basis): Dedekind's linear independence of characters (#1595)

kckennylau committed 6 years ago

8eaf478a

feat(data/nat): a lemma about min_fac (#1603)

kim-em committed 6 years ago

b9798dc7

feat(data/set/intervals): fintype instances for ℕ and ℤ (#1602)

kim-em committed 6 years ago

b46f5b04

refactor(data/rat/meta): rename to meta_defs (#1612)

robertylewis committed 6 years ago

6ee8bf97

chore(data/nat/basic): remove pos_iff_ne_zero' (#1610)

rwbarton committed 6 years ago

9db43a5f

feat(meta/expr,data/rat/basic): add rat.reflect (#1565)

robertylewis committed 6 years ago

151bcbe2

chore(category_theory): replace some @[simp] with @[simps] (#1605)

kim-em committed 6 years ago

3f8a492b

chore(group_theory/free_group,order/zorn): rename zorn.zorn and sum.sum (#1604)

robertylewis committed 6 years ago

b1f44ba1

Older