leanprover-community/mathlib3

Pull Requests Commits

chore(*): don't assume `sub_eq_add_neg` and `div_eq_mul_inv` are defeq (#5302)

Vierkantor committed 5 years ago

a372dfce

feat(ring_theory/witt_vector): truncated Witt vectors, definition and ring structure (#5162)

jcommelin committed 5 years ago

d2ae4e25

feat(linear_algebra/alternating): Add alternatization of multilinear_map (#5187)

eric-wieser committed 5 years ago

6288eeda

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

leanprover-community-bot committed 5 years ago

dbdba555

chore(linear_algebra/tensor_product): Relax the ring requirement to semiring for the group instance (#5305)

eric-wieser committed 5 years ago

8817c3ea

feat(topology/separation): finite t1 spaces are discrete (#5298)

adomani committed 5 years ago

9e550f2d

feat(combinatorics/simple_graph/degree_sum): degree-sum formula and handshake lemma (#5263)

agusakov committed 5 years ago

2c0b43d9

chore(data/finsupp/basic): redefine `finsupp.filter` (#5310)

urkud committed 5 years ago

918d5a95

feat(algebra/module/basic): {nat,int}_smul_apply (#5308)

jcommelin committed 5 years ago

c2958736

chore(data/mv_polynomial): delete stray comments (#5312)

robertylewis committed 5 years ago

c9793b52

chore(data/complex/exponential): add `inv_one_add_tan_sq` etc (#5299)

urkud committed 5 years ago

f72734a3

feat(category_theory/monad): special coequalizers for a monad (#5239)

b-mehta committed 5 years ago

32b2e305

feat(algebra/group/hom): add_monoid_hom.sub_apply (#5307)

jcommelin committed 5 years ago

4e8486b8

feat(algebra/big_operators/finsupp): rename variables, and move to top of file (#5306)

jcommelin committed 5 years ago

be6c37ce

chore(linear_algebra/determinant): Golf a proof (#5309)

eric-wieser committed 5 years ago

f3c9d204

feat(category_theory/limits): any functor preserves split coequalizers (#5246)

b-mehta committed 5 years ago

cdb13984

feat(category_theory/sites/sieves): change presieve operation defs (#5295)

b-mehta committed 5 years ago

12d097e3

feat(group_theory/perm/sign): Add sign_sum_congr (#5266)

eric-wieser committed 5 years ago

3f42fb48

refactor(order/filter/ultrafilter): drop `filter.is_ultrafilter` (#5264)

urkud committed 5 years ago

90755c36

feat(group_theory/group_action/sub_mul_action): add a has_zero instance (#5216)

eric-wieser committed 5 years ago

2bf0c2e7

refactor(data/finsupp/basic): merge `finsupp.of_multiset` and `multiset.to_finsupp` (#5237)

urkud committed 5 years ago

702b1e8c

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

Older