leanprover-community/mathlib

Pull Requests Commits

urkud committed 5 years ago

9b58f539

Merge branch 'mazur-ulam-affine' into bundle-direction

urkud committed 5 years ago

4a72c6cb

urkud committed 5 years ago

b081bbac

Merge branch 'master' into bundle-direction

urkud committed 5 years ago

1ac56abf

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

Merge branch 'master' into bundle-direction

urkud committed 5 years ago

e6785074

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

b-mehta committed 5 years ago

f2793132

Add a docstring

urkud committed 5 years ago

1f56bd6a

urkud committed 5 years ago

8c9ae0a4

Merge branch 'master' into mazur-ulam-affine

urkud committed 5 years ago

75de3268

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

leanprover-community-bot committed 5 years ago

8bd1df59

urkud committed 5 years ago

bf9ac4e1

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

faenuccio committed 5 years ago

de12036b

Merge branch 'affine-equiv' into mazur-ulam-affine

urkud committed 5 years ago

4dc0bee8

Merge branch 'master' into affine-equiv

urkud committed 5 years ago

27c801a4

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

Older