leanprover-community/mathlib

Pull Requests Commits

feat(data/list/basic): Add prod_reverse_noncomm (#4757)

eric-wieser committed 5 years ago

c141eed8

feat(algebra/direct_sum): Bundle the homomorphisms (#4754)

eric-wieser committed 5 years ago

4ec88dbe

feat(category_theory): presheaf is colimit of representables (#4401)

b-mehta committed 5 years ago

aa590397

chore(*): a few more type-specific ext lemmas (#4741)

urkud committed 5 years ago

5afeb9b9

fix(deprecated/group): Correct the name of `is_add_group_hom has_neg.neg` (#4755)

eric-wieser committed 5 years ago

0bbf3e29

feat(data/{nat,list}/basic): Add some trivial lemmas (#4738)

eric-wieser committed 5 years ago

58869614

feat(tactic/core): add `run_parser` user command (#4745)

digama0 committed 5 years ago

b651c6f6

fix(deprecated/*): remove instances (#4735)

jcommelin committed 5 years ago

fb4aee0d

refactor(*): use is_scalar_tower instead of restrict_scalars (#4733)

jcommelin committed 5 years ago

70b14cee

feat(ring_theory/roots_of_unity): Roots of unity as union of primitive roots (#4644)

riccardobrasca committed 5 years ago

82b4843c

feat(analysis/p_series): prove the p-series convergence test (#4360)

urkud committed 5 years ago

278a14b3

feat(ring_theory/witt_vector/defs): type of witt vectors + ring operations (#4332)

jcommelin committed 5 years ago

04b55727

feat(linear_algebra/affine_space): define `affine_equiv.mk'` (#4750)

urkud committed 5 years ago

9e4ef854

chore(topology/*): add two missing simp coe lemmas (#4748)

urkud committed 5 years ago

468c01c8

chore(algebra/group/basic): Mark inv_involutive simp (#4744)

eric-wieser committed 5 years ago

458c833e

feat(linear_algebra/basic): define `linear_equiv.neg` (#4749)

urkud committed 5 years ago

bb52355b

refactor(*): lmul is an algebra hom (#4724)

jcommelin committed 5 years ago

dc4ad812

feat(measure_theory/measure_space): Added lemmas for commuting restrict for outer measures and measures (#4673)

mzinkevi committed 5 years ago

ff711a31

feat(category_theory/yoneda): better simp lemmas for small yoneda (#4743)

b-mehta committed 5 years ago

f2793132

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

leanprover-community-bot committed 5 years ago

8bd1df59

chore(data/polynomial): remove monomial_one_eq_X_pow (#4734)

faenuccio committed 5 years ago

de12036b

chore(data/equiv/basic): Add a simp lemma perm.coe_mul (#4723)

eric-wieser committed 5 years ago

6eb55641

chore(*): 3 unrelated small changes (#4732)

urkud committed 5 years ago

add50960

feat(algebra/monoid_algebra): define a non-commutative version of `lift` (#4725)

urkud committed 5 years ago

aba31c93

feat(linear_algebra/nonsingular_inverse): state Cramer's rule explicitly (#4700)

Oliver Nash committed 5 years ago

fb5ef2b9

refactor(algebra/add_torsor): define pointwise `-ᵥ` and `+ᵥ` on sets (#4710)

urkud committed 5 years ago

03f0285d

feat(algebra/gcd_monoid): noncomputably defines `gcd_monoid` structures from partial information (#4664)

awainverse committed 5 years ago

4c4d47c2

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

leanprover-community-bot committed 5 years ago

fca876ea

feat(archive): formalize compiler correctness by McCarthy and Painter (#4702)

xiw committed 5 years ago

df450024

feat(linear_algebra/affine_space): define `affine_equiv` (#2909)

urkud committed 5 years ago

1b4e7694

Newer Older