leanprover-community/mathlib

Pull Requests Commits

kim-em committed 5 years ago

53c34bab

kim-em committed 5 years ago

a5a9c54d

trying to automate that compactness is hygienic

kim-em committed 5 years ago

24a793aa

a derive handler

kim-em committed 5 years ago

58018ef9

Merge remote-tracking branch 'origin/315' into iso_transport

kim-em committed 5 years ago

1d885362

kim-em committed 5 years ago

8034d445

Fix misleading comment.

gebner committed 5 years ago

32316360

kim-em committed 5 years ago

f9c0ea69

kim-em committed 5 years ago

135881cc

kim-em committed 5 years ago

e2410a68

kim-em committed 5 years ago

f0660b79

kim-em committed 5 years ago

9ccfde6f

kim-em committed 5 years ago

d8498d2d

use one := 1 advice for field.to_euclidean_domain

ChrisHughes24 committed 5 years ago

9b946bf9

Merge branch '315' of https://github.com/leanprover-community/mathlib into HEAD

ChrisHughes24 committed 5 years ago

9e7ed943

delete `dual.vector_space`

ChrisHughes24 committed 5 years ago

201fcfcb

Merge remote-tracking branch 'origin/master' into HEAD

ChrisHughes24 committed 5 years ago

f557dd26

Merge remote-tracking branch 'community/master' into 315

bryangingechen committed 5 years ago

208f5e55

chore(algebra/group_hom): rename `add_monoid.smul` to `nsmul` (#2861)

urkud committed 5 years ago

a285049b

chore(data/set/basic): add some lemmas to `function.surjective` (#2876)

urkud committed 5 years ago

28e79d48

feat(topology/homeomorph): sum_prod_distrib (#2870)

rwbarton committed 5 years ago

297806e6

feat(tactic/noncomm_ring): add noncomm_ring tactic (#2858)

Oliver Nash committed 5 years ago

0827a30c

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

leanprover-community-bot committed 5 years ago

6e581ef2

chore(order/bounds): +2 lemmas, fix a name (#2877)

urkud committed 5 years ago

c034b4c2

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

leanprover-community-bot committed 5 years ago

9d76ac24

feat(group_theory/group_action): orbit_equiv_quotient_stabilizer_symm_apply and docs (#2864)

kckennylau committed 5 years ago

f05acc8e

refactor(algebra/module): change module into an abbreviation for semimodule (#2848)

urkud committed 5 years ago

67f1951b

feat(algebra/big_operators): prod_ne_zero (#2863)

kckennylau committed 5 years ago

cc06d538

chore(topology): make topological_space fields protected (#2867)

rwbarton committed 5 years ago

b40ac2af

feat(geometry/euclidean): Euclidean space (#2852)

jsm28 committed 5 years ago

62cb7f2f

Older