leanprover-community/mathlib3

Pull Requests Commits

feat(data/equiv): symm_symm_apply (#5324)

b-mehta committed 5 years ago

846ee3f4

chore(group_theory/perm/basic): Add missing lemmas (#5320)

eric-wieser committed 5 years ago

63e1ad43

chore(algebra/big_operators/basic): Rename hypotheses for clarity (#5318)

eric-wieser committed 5 years ago

90aa66bf

chore(data/subtype): Add coind_bijective and map_involutive (#5319)

eric-wieser committed 5 years ago

3a88a9ea

chore(linear_algebra/tensor_product): Actually relax the requirements for add_comm_group (#5315)

eric-wieser committed 5 years ago

029b2587

chore(*): simp lemmas for `tendsto`, `Ixx`, and `coe` (#5296)

urkud committed 5 years ago

db712d59

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

Newer Older