leanprover-community/mathlib3

Pull Requests Commits
typo
bottine committed 3 years ago
29452afe
Junyan's suggestions
bottine committed 3 years ago
bfbb7480
lint
bottine committed 3 years ago
b7b02cfa
minor things
bottine committed 3 years ago
587cf96c
minor things
bottine committed 3 years ago
98de114d
it typechecks
bottine committed 3 years ago
58d54abe
barh
bottine committed 3 years ago
9b0052b5
trying to organize things
bottine committed 3 years ago
c7d92861
trying to organize things
bottine committed 3 years ago
11f80bf4
so that #lint doesn't complain
bottine committed 3 years ago
59f2647a
yes
bottine committed 3 years ago
ad891001
yes
bottine committed 3 years ago
418d3d5b
this and that
bottine committed 3 years ago
453b8c5b
TODO'd lemma done
bottine committed 3 years ago
1b7a7df1
moving things where I think they belong
bottine committed 3 years ago
2533e44f
commit just to get the CI to build mathlib for me
bottine committed 3 years ago
66a1d36b
commit just to get the CI to build mathlib for me
bottine committed 3 years ago
c30b11aa
yes
bottine committed 3 years ago
e4202efd
starting to reorganize towards PR?
bottine committed 3 years ago
15393f4c
merge master
bottine committed 3 years ago
8a25bc3d
@alreadydone's code
bottine committed 3 years ago
408e87fa
fix(*/finsupp/*): add missing decidable arguments in lemma statements (#18251)
eric-wieser committed 3 years ago
6e492fdb
feat(data/tree): Add definitions about binary trees; special support for `tree unit` (#16715)
prakol16 committed 3 years ago
ed989ff5
doc(computability/primrec): remove doc nolints (#16018)
vihdzp committed 3 years ago
959c3b69
chore(field_theory/minpoly/*): replace `gcd_monoid.lean` by `is_integrally_closed.lean` and remove results that have been generalized (#18206)
Paul-Lez committed 3 years ago
2032a878
refactor(data/set/finite): reduce imports (#18245)
urkud committed 3 years ago
1f0096e6
chore(analysis/von_neumann_algebra/basic): add missing API lemmas (#18227)
eric-wieser committed 3 years ago
160ef3e3
feat(special_functions/trigonometric/bounds): Add the inequality `cos x < 1 / sqrt (x ^ 2 + 1)` (#18189)
loefflerd committed 3 years ago
9df54c1b
feat(data/nat/hyperoperation): Defined hyperoperation and added related lemmas (#18116)
Nazgand committed 3 years ago
386c02e7
fix(order/filter/basic): fix a diamond (#18255)
urkud committed 3 years ago
71efed1b
Terms Of Use Privacy Policy Refund Policy Impressum