leanprover-community/mathlib3

Pull Requests Commits

Merge remote-tracking branch 'mathlib/master' into bundle_has_sub_div

Vierkantor committed 5 years ago

136b102e

chore(category_theory/limits/preserves): cleanup (#4163)

b-mehta committed 5 years ago

ac669c74

feat(category_theory/sites): category of sheaves (#5255)

b-mehta committed 5 years ago

e68d2d78

chore(scripts): update nolints.txt (#5297)

leanprover-community-bot committed 5 years ago

ba568a61

chore(data/indicator_function): a few more `simp` lemmas (#5293)

urkud committed 5 years ago

84c0132e

chore(data/set/intervals/proj_Icc): add `strict_mono_incr_on` (#5292)

urkud committed 5 years ago

bf25d26f

feat(measure_theory/interval_integral): continuous implies interval_integrable (#5288)

hrmacbeth committed 5 years ago

efe18d5d

chore(linear_algebra/multilinear): Add `linear_map.comp_multilinear_map_dom_dom_congr` (#5270)

eric-wieser committed 5 years ago

e357a338

ci(.github/workflows/dependent-issues.yml): automation for "blocked-by-other-PR" label (#5261)

bryangingechen committed 5 years ago

698d6b76

feat(category_theory/limits/preserves): preserving binary products (#5061)

b-mehta committed 5 years ago

a87f62bc

chore(data/mv_polynomial): mark `mv_polynomial.ext` as `@[ext]` (#5289)

urkud committed 5 years ago

d12a7319

feat(analysis/special_functions): `real.log` is infinitely smooth away from zero (#5116)

urkud committed 5 years ago

1f309c52

chore(scripts): update nolints.txt (#5287)

leanprover-community-bot committed 5 years ago

2032f7ba

chore(data/pi): Express `single` in terms of `function.update` (#5283)

eric-wieser committed 5 years ago

7ae11651

chore(data/equiv/mul_add): Split out the group structure on automorphisms (#5281)

eric-wieser committed 5 years ago

1e3447b8

chore(algebra/group/pi): Split into multiple files (#5280)

eric-wieser committed 5 years ago

4c9499fc

feat(topology/algebra/ordered): add lemmas about `map coe at_top/at_bot` (#5238)

urkud committed 5 years ago

b5ab2f77

feat(category_theory/limits): split coequalizers (#5230)

b-mehta committed 5 years ago

7f5a5ddd

feat(analysis/mean_inequalities): add Hölder's inequality for the Lebesgue integral of ennreal and nnreal functions (#5267)

RemyDegenne committed 5 years ago

64ddb126

chore(logic/basic): add a few `simp` lemmas (#5278)

urkud committed 5 years ago

3996bd42

chore(combinatorics/composition): use `order_embedding` (#5276)

urkud committed 5 years ago

d3bbaeb9

chore(group_theory/perm): Add alternate formulation of (sum|sigma)_congr lemmas (#5260)

eric-wieser committed 5 years ago

51f5ca3e

chore(*): move/add lemmas about `disjoint` (#5277)

urkud committed 5 years ago

ac6fc38e

chore(data/list/sort): docs, add a few lemmas (#5274)

urkud committed 5 years ago

ef377a92

feat(category_theory/monad): generalise algebra colimits (#5234)

b-mehta committed 5 years ago

aec64b17

feat(category_theory/closed/types): presheaf category is cartesian closed (#4897)

b-mehta committed 5 years ago

73601789

chore(data/list/pairwise): add `list.pairwise_pmap` and `list.pairwise.pmap` (#5273)

urkud committed 5 years ago

8f42d73d

chore(data/support): zero function has empty support (#5275)

urkud committed 5 years ago

3f4829cd

chore(scripts): update nolints.txt (#5272)

leanprover-community-bot committed 5 years ago

35f08626

refactor(data/fin): use `order_embedding` for many maps (#5251)

urkud committed 5 years ago

b173925a

Older