leanprover-community/mathlib3

Pull Requests Commits

removing the old `functor.of`

Scott Morrison committed 6 years ago

28dae2bc

feat(category_theory/functorial): unbundled functors

Scott Morrison committed 6 years ago

31ef79d3

kim-em committed 6 years ago

ec618c1a

Merge remote-tracking branch 'origin/master' into category_no_sorts

kim-em committed 6 years ago

d9700b92

chore(category_theory/functor_category): improve comment warning about hcomp_assoc [ci skip] (#1434)

kim-em committed 6 years ago

590fb896

feat(well_founded_tactics): patch default_dec_tac (#1419)

kim-em committed 6 years ago

140a606a

chore(*): renaming files constructing category instances (#1432)

kim-em committed 6 years ago

e27142aa

fix(algebra/*/colimits): avoid explicit `infer_instance` (#1430)

urkud committed 6 years ago

8a5156fc

feat(logic): make some decidability proofs [inline] (#1393)

fpvandoorn committed 6 years ago

45fe081f

chore(algebra/group/to_additive): map_namespace should make a meta constant (#1409)

ChrisHughes24 committed 6 years ago

8e46fa5a

feat(tactic/auto_cases): run auto_cases on false and psigma (#1428)

kim-em committed 6 years ago

e2f904ec

feat(tactic/{abel,ring}): state conditions of tactics more precisely (#1423)

kappelmann committed 6 years ago

c87ec0e4

let simp flip inequalities (#1418)

kim-em committed 6 years ago

2dd6398e

feat(algebra/group/units): add some lemmas about `divp` (#1388)

urkud committed 6 years ago

0935e8bf

chore(topology): sanity_check pass (#1416)

sgouezel committed 6 years ago

fe1575a0

feat(sanity_check): greatly improve performance (#1389)

fpvandoorn committed 6 years ago

72d6325a

feat(algebra/big_operators): sum_eq_zero_iff_of_nonpos (#1424)

ChrisHughes24 committed 6 years ago

228d5bad

feat(algebra/floor): Split floor from archimedean file. (#1372)

kappelmann committed 6 years ago

313fe11b

feat(data/list/basic): make chain.nil a simp lemma (#1414)

kim-em committed 6 years ago

37b67460

feat(data/list/defs): move list.sum to list/defs.lean (#1415)

kim-em committed 6 years ago

6f7224cc

feat(topology/local_homeomorph): local homeomorphisms (#1398)

sgouezel committed 6 years ago

8bdb1474

feat(topology/constructions): distributivity of products over sums (#1059)

rwbarton committed 6 years ago

10cb0d12

refactor(category_theory/limits/shapes/pullbacks): proof golf (#1407)

rwbarton committed 6 years ago

d6a0ac58

refactor(category_theory/limits): make is_[co]limit not a class (#1405)

rwbarton committed 6 years ago

8eab714f

fix(category_theory/limits/shapes): doc typo [ci skip] (#1406)

rwbarton committed 6 years ago

a7f268b8

chore(data/mv_polynomial): use classical logic (#1391)

kim-em committed 6 years ago

a5fa162b

move back to Type

kim-em committed 6 years ago

647b9ece

chore(category_theory): require morphisms live in Type

kim-em committed 6 years ago

3a394670

fix(naming): typo [ci skip] (#1401)

fpvandoorn committed 6 years ago

1a0ed809

chore(algebra/ordered_field): add simp attributes to inv_pos' and others (#1400)

ChrisHughes24 committed 6 years ago

b1920f59

Older