Commits

Branch selector

 master

User selector

All users

All time

Commit history

Commits on Apr 19, 2020

• chore(number_theory/sum_four_squares): slightly shorten proof (#2457)

  Show description for 6054f7c
  ChrisHughes24

  committed
  6054f7c

  Copy full SHA for 6054f7c

• chore(category_theory/monoidal): some arguments that need to be made explicit in 3.8

  kim-em

  committed
  d344310

  Copy full SHA for d344310

• chore(algebra/module): replace typeclass arguments with inferred arguments (#2444)

  Show description for 11d89a2
  

  kim-em

  and

  Scott Morrison

  committed
  11d89a2

  Copy full SHA for 11d89a2

• feat(data/nat/prime) factors of a prime number is the list [p] (#2452)

  Show description for 0ceac44
  

  alexjbest

  and

  kim-em

  committed
  0ceac44

  Copy full SHA for 0ceac44

Commits on Apr 18, 2020

• chore(*): switch to lean 3.9.0 (#2449)

  Show description for 99245b3
  gebner

  committed
  99245b3

  Copy full SHA for 99245b3

• feat(category_theory/limits/over): over category has connected limits (#2438)

  Show description for d76a882
  

  b-mehta

  and

  Scott Morrison

  committed
  d76a882

  Copy full SHA for d76a882

• fix(*): remove `@[nolint simp_nf]` (#2450)

  Show description for 8ec447d
  gebner

  committed
  8ec447d

  Copy full SHA for 8ec447d

• fix(docs/extra/calc.md): remove extra space (#2448)

  Show description for 5107c2b
  bryangingechen

  committed
  5107c2b

  Copy full SHA for 5107c2b

• fix(group_theory/submonoid): looping simp lemma (#2447)

  Show description for 16552e6
  gebner

  committed
  16552e6

  Copy full SHA for 16552e6

• feat(tactic/transport): transport structures across equivalences (#2251)

  Show description for 4e87223
  kim-em

  committed
  4e87223

  Copy full SHA for 4e87223

• chore(algebra/group/type_tags): add `additive.to_mul` etc (#2363)

  Show description for ffb99a3
  

  urkud

  and

  gebner

  committed
  ffb99a3

  Copy full SHA for ffb99a3

• chore(data/mv_polynomial): adding a comment about a T50000 regression (#2442)

  Show description for 8b21231
  

  kim-em

  and

  Scott Morrison

  committed
  8b21231

  Copy full SHA for 8b21231

• refactor(data/nat/fib): simplify proof of fib_succ_succ (#2443)

  Show description for a530a81
  lambda-fairy

  committed
  a530a81

  Copy full SHA for a530a81

• docs(install/*): put extra emphasis (#2439)

  Show description for 1ef989f
  

  3 peoplecommitted
  1ef989f

  Copy full SHA for 1ef989f

• feat(tactic/lint): lint for missing has_coe_to_fun instances (#2437)

  Show description for 6b09575
  gebner

  committed
  6b09575

  Copy full SHA for 6b09575

Commits on Apr 17, 2020

• fix(github/workflows): ignore new bors branch (#2441)

  Show description for 24d464c
  gebner

  committed
  24d464c

  Copy full SHA for 24d464c

• chore(scripts): update nolints.txt (#2440)

  Show description for da29275
  

  leanprover-community-bot

  committed
  da29275

  Copy full SHA for da29275

• chore(*): migrate `nat/int/rat.eq_cast` to bundled homs (#2427)

  Show description for 64f6903
  

  3 peoplecommitted
  64f6903

  Copy full SHA for 64f6903

• feat(data/nat): Results about nat.choose (#2421)

  Show description for 855e70b
  b-mehta

  committed
  855e70b

  Copy full SHA for 855e70b

• feat(analysis/analytic/composition): the composition of analytic functions is analytic (#2399)

  Show description for 0bc15f8
  

  sgouezel

  and

  kim-em

  committed
  0bc15f8

  Copy full SHA for 0bc15f8

• chore(scripts): update nolints.txt (#2436)

  Show description for 715be9f
  

  leanprover-community-bot

  committed
  715be9f

  Copy full SHA for 715be9f

• feat(category_theory/limits): strong epimorphisms and strong epi-mono factorizations (#2433)

  Show description for 0567b7f
  TwoFX

  committed
  0567b7f

  Copy full SHA for 0567b7f

• feat(category_theory): creation of limits and reflection of isomorphisms (#2426)

  Show description for f347147
  

  b-mehta

  and

  Scott Morrison

  committed
  f347147

  Copy full SHA for f347147

• chore(scripts): update nolints.txt (#2435)

  Show description for 0d3e546
  

  leanprover-community-bot

  committed
  0d3e546

  Copy full SHA for 0d3e546

• chore(algebra/lie_algebra): add function coercion for morphisms (#2434)

  Show description for d2db3e8
  

  Oliver Nash

  committed
  d2db3e8

  Copy full SHA for d2db3e8

Commits on Apr 16, 2020

• feat(computability): strong reducibility and degrees (#1203)

  Show description for c3d943e
  

  3 peoplecommitted
  c3d943e

  Copy full SHA for c3d943e

• chore(scripts): update nolints.txt (#2432)

  Show description for a113d6e
  

  leanprover-community-bot

  committed
  a113d6e

  Copy full SHA for a113d6e

• feat(analysis/calculus): let simp compute derivatives (#2422)

  Show description for 846cbab
  sgouezel

  committed
  846cbab

  Copy full SHA for 846cbab

• refactor(analysis/asymptotics): make is_o irreducible (#2416)

  Show description for ec80061
  sgouezel

  committed
  ec80061

  Copy full SHA for ec80061

• refactor(tactic/norm_cast): simplified attributes and numeral support (#2407)

  Show description for 5fd4afc
  

  gebner

  and

  Paul-Nicolas Madelaine

  committed
  5fd4afc

  Copy full SHA for 5fd4afc

• chore(scripts): update nolints.txt (#2430)

  Show description for 7270af9
  

  leanprover-community-bot

  committed
  7270af9

  Copy full SHA for 7270af9

• feat(category_theory): connected categories (#2413)

  Show description for 5ac2b48
  b-mehta

  committed
  5ac2b48

  Copy full SHA for 5ac2b48

Commits on Apr 15, 2020

• feat(data/finset): existence of a smaller set (#2420)

  Show description for 66cc298
  b-mehta

  committed
  66cc298

  Copy full SHA for 66cc298

• chore(scripts): update nolints.txt (#2425)

  Show description for 8510f07
  

  leanprover-community-bot

  committed
  8510f07

  Copy full SHA for 8510f07

• fix(data/zmod/basic): typo (#2424)

  kbuzzard

  committed
  1e212d7

  Copy full SHA for 1e212d7