Commits

Branch selector

 master

User selector

All users

All time

Commit history

Commits on Nov 5, 2019

• docs(tactic/lint) add code fence around #print statement to avoid its args looking like html tags.

  ratmice

  committed
  3a948a6

  Copy full SHA for 3a948a6

• refactor(sum_two_square): extract lemmas about primes in Z[i] (#1643)

  Show description for 986e58c
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  986e58c

  Copy full SHA for 986e58c

Commits on Nov 4, 2019

• feat(floor): one more lemma (#1646)

  Show description for f3f1fd8
  

  2 peopleauthored and

  mergify[bot]

  committed
  f3f1fd8

  Copy full SHA for f3f1fd8

• fix(tactic/tfae,scc): change the strongly connected component algorithm (#1600)

  Show description for 2dcc6c2
  

  cipher1024

  authored and

  mergify[bot]

  committed
  2dcc6c2

  Copy full SHA for 2dcc6c2

• feat(simps): allow the user to specify the projections (#1630)

  Show description for ee5b38d
  

  fpvandoorn

  authored and

  mergify[bot]

  committed
  ee5b38d

  Copy full SHA for ee5b38d

Commits on Nov 3, 2019

• feat(analysis/normed_space): Riesz's lemma (#1642)

  Show description for a6ace34
  

  jlpaca

  authored and

  mergify[bot]

  committed
  a6ace34

  Copy full SHA for a6ace34

Commits on Nov 1, 2019

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

  Show description for 9af7e5b
  

  2 peopleauthored and

  mergify[bot]

  committed
  9af7e5b

  Copy full SHA for 9af7e5b

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

  Show description for 1710fd8
  

  fpvandoorn

  authored and

  mergify[bot]

  committed
  1710fd8

  Copy full SHA for 1710fd8

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

  Show description for 5f17abc
  

  2 peopleauthored and

  mergify[bot]

  committed
  5f17abc

  Copy full SHA for 5f17abc

Commits on Oct 31, 2019

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

  Show description for df91623
  

  kim-em

  authored and

  mergify[bot]

  committed
  df91623

  Copy full SHA for df91623

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

  Show description for cd0bc32
  

  kim-em

  authored and

  mergify[bot]

  committed
  cd0bc32

  Copy full SHA for cd0bc32

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

  

  gebner

  authored and

  mergify[bot]

  committed
  6b51787

  Copy full SHA for 6b51787

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

  Show description for 780cbc9
  

  2 peopleauthored and

  mergify[bot]

  committed
  780cbc9

  Copy full SHA for 780cbc9

Commits on Oct 30, 2019

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

  

  robertylewis

  authored and

  mergify[bot]

  committed
  d43f7f9

  Copy full SHA for d43f7f9

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

  Show description for aadfde6
  

  2 peopleauthored and

  mergify[bot]

  committed
  aadfde6

  Copy full SHA for aadfde6

Commits on Oct 29, 2019

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

  Show description for ca90081
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  ca90081

  Copy full SHA for ca90081

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

  

  kim-em

  authored and

  mergify[bot]

  committed
  6030ff0

  Copy full SHA for 6030ff0

• cleanup(order|string) (#1629)

  Show description for e6e25d0
  

  fpvandoorn

  authored and

  mergify[bot]

  committed
  e6e25d0

  Copy full SHA for e6e25d0

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

  Show description for b9e3dbb
  

  fpvandoorn

  authored and

  mergify[bot]

  committed
  b9e3dbb

  Copy full SHA for b9e3dbb

• fix(*): use has_coe_t (#1627)

  

  fpvandoorn

  authored and

  mergify[bot]

  committed
  b5b674c

  Copy full SHA for b5b674c

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

  Show description for 0ea3dfe
  

  cipher1024

  authored and

  mergify[bot]

  committed
  0ea3dfe

  Copy full SHA for 0ea3dfe

Commits on Oct 28, 2019

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

  Show description for 7a8f53e
  

  robertylewis

  authored and

  mergify[bot]

  committed
  7a8f53e

  Copy full SHA for 7a8f53e

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

  Show description for 94e368c
  

  ChrisHughes24

  authored and

  mergify[bot]

  committed
  94e368c

  Copy full SHA for 94e368c

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

  Show description for c2e81dd
  

  skbaek

  authored and

  mergify[bot]

  committed
  c2e81dd

  Copy full SHA for c2e81dd

Commits on Oct 27, 2019

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

  Show description for 1fa03c2
  

  Oliver Nash

  authored and

  mergify[bot]

  committed
  1fa03c2

  Copy full SHA for 1fa03c2

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

  Show description for 89ece14
  

  rwbarton

  authored and

  mergify[bot]

  committed
  89ece14

  Copy full SHA for 89ece14

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

  

  kim-em

  authored and

  mergify[bot]

  committed
  8a45d98

  Copy full SHA for 8a45d98

Commits on Oct 26, 2019

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

  Show description for 8eaf478
  

  kckennylau

  authored and

  mergify[bot]

  committed
  8eaf478

  Copy full SHA for 8eaf478

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

  Show description for b9798dc
  

  kim-em

  authored and

  mergify[bot]

  committed
  b9798dc

  Copy full SHA for b9798dc

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

  Show description for b46f5b0
  

  kim-em

  authored and

  mergify[bot]

  committed
  b46f5b0

  Copy full SHA for b46f5b0

Commits on Oct 25, 2019

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

  Show description for 6ee8bf9
  

  robertylewis

  authored and

  mergify[bot]

  committed
  6ee8bf9

  Copy full SHA for 6ee8bf9

Commits on Oct 24, 2019

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

  Show description for 9db43a5
  

  rwbarton

  authored and

  mergify[bot]

  committed
  9db43a5

  Copy full SHA for 9db43a5

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

  Show description for 151bcbe
  

  robertylewis

  authored and

  mergify[bot]

  committed
  151bcbe

  Copy full SHA for 151bcbe

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

  

  kim-em

  authored and

  mergify[bot]

  committed
  3f8a492

  Copy full SHA for 3f8a492

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

  Show description for b1f44ba
  

  robertylewis

  authored and

  mergify[bot]

  committed
  b1f44ba

  Copy full SHA for b1f44ba