Commits

Breadcrumbs

History for

onmaster

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(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

• 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

• 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

• 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(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

• 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

• 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

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

  kbuzzard

  committed
  1e212d7

  Copy full SHA for 1e212d7

• feat(category_theory/limits): special shapes API cleanup (#2423)

  Show description for ce72cde
  TwoFX

  committed
  ce72cde

  Copy full SHA for ce72cde

• feat(library_search): (efficiently) try calling symmetry before searching the library (#2415)

  Show description for 9b797ee
  

  3 peoplecommitted
  9b797ee

  Copy full SHA for 9b797ee

• chore(category_theory/limits): remove dependency on concrete_categories (#2411)

  Show description for 8e8037f
  

  kim-em

  and

  Scott Morrison

  committed
  8e8037f

  Copy full SHA for 8e8037f

Commits on Apr 14, 2020

• refactor(analysis/calculus/deriv): split comp and scomp (#2410)

  Show description for 96a07a7
  sgouezel

  committed
  96a07a7

  Copy full SHA for 96a07a7

• feat(algebra/lie_algebra): define equivalences, direct sums of Lie algebras (#2404)

  Show description for 15fcb8a
  

  ocfnash

  committed
  15fcb8a

  Copy full SHA for 15fcb8a

• fix(library_search): find id (#2414)

  Show description for ba154bc
  kim-em

  committed
  ba154bc

  Copy full SHA for ba154bc

• chore(analysis): two more -T50000 challenges (#2393)

  Show description for af27ee3
  kim-em

  committed
  af27ee3

  Copy full SHA for af27ee3

Commits on Apr 13, 2020

• feat(logic/basic): a few simp lemmas about `and` and `or` (#2408)

  ChrisHughes24

  committed
  8356b79

  Copy full SHA for 8356b79

• feat(algebra/big-operators): some big operator lemmas (#2152)

  Show description for fe878ea
  b-mehta

  committed
  fe878ea

  Copy full SHA for fe878ea