leanprover-community/mathlib3

Pull Requests Commits
stating the abc conjecture
kim-em committed 4 years ago
69c9b105
Update .docker/README.md
kim-em committed 4 years ago
Verified 4d8199a5
Add instructions for use in other repos
kim-em committed 4 years ago
f8db5037
rename leanprover to leanprovercommunity
kim-em committed 4 years ago
9e61d91d
tweak comments
kim-em committed 4 years ago
059297e1
Update .devcontainer/README.md
kim-em committed 4 years ago
Verified 45ac3269
Update .docker/alpine/lean/Dockerfile
kim-em committed 4 years ago
Verified 6f6987a2
nope, gitpod doesn't like our debian container, either
kim-em committed 4 years ago
9e35a8cb
experimenting with the debian container on gitpod
kim-em committed 4 years ago
7dbd25a4
experimenting with the alpine container on gitpod
kim-em committed 4 years ago
6b7b289f
experiment with no version number for VSCode extension
kim-em committed 4 years ago
e405fbf5
more optimisation
kim-em committed 4 years ago
75c349b7
improvements
kim-em committed 4 years ago
505f1a2b
shrink the alpine image
kim-em committed 4 years ago
e7010467
oops
kim-em committed 4 years ago
8565edd4
oops
kim-em committed 4 years ago
bbff6026
add badges, suppress error message
kim-em committed 4 years ago
59847a54
separate README
kim-em committed 4 years ago
8817ff30
separate README
kim-em committed 4 years ago
d7e3bf25
linkify URLs
kim-em committed 4 years ago
da2cdd8a
note on deployment
kim-em committed 4 years ago
c0590c9f
feat(.docker): Docker containers for debian, ubuntu, and gitpod
kim-em committed 4 years ago
6fe6951a
feat(algebra/big_operators/basic): lemmas prod_range_add, sum_range_add (#6484)
Nazgand committed 4 years ago
22e34370
refactor(ring_theory/valuation): valuations in `linear_ordered_comm_monoid_with_zero` (#6500)
awainverse committed 4 years ago
19ed0f8e
feat(ring_theory/polynomial/chebyshev/basic): multiplication of Chebyshev polynomials (#6501)
hrmacbeth committed 4 years ago
0c5b5172
refactor(data/set/finite): change type of `set.finite.dependent_image` (#6475)
urkud committed 4 years ago
0c863e98
refactor(data/set/finite): make `finite` argument of `set.finite.mem_to_finset` explicit (#6508)
urkud committed 4 years ago
c0870115
feat(data/{nat,int}/parity): even_mul_succ_self (#6507)
pechersky committed 4 years ago
9f0f05ee
feat(data/finset/lattice): +2 induction principles for `finset`s (#6502)
urkud committed 4 years ago
6b5e48d7
chore(algebra/big_operators): use weaker typeclass assumptions (#6503)
urkud committed 4 years ago
572f7274
Terms Of Use Privacy Policy Refund Policy Impressum