Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat port Data.Int.Gcd #981

Closed
wants to merge 45 commits into from
Closed

[Merged by Bors] - feat port Data.Int.Gcd #981

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
45 commits
Select commit Hold shift + click to select a range
1abf228
feat port Data.Int.Gcd
riccardobrasca Dec 13, 2022
0ea070b
update mathlib.lean
riccardobrasca Dec 13, 2022
3ebd0d8
start fixing stuff
riccardobrasca Dec 13, 2022
5f69f40
little progress
riccardobrasca Dec 13, 2022
4501070
Merge branch 'master' into RB/int.gcd
riccardobrasca Dec 14, 2022
6f27478
initial commit
mcdoll Dec 15, 2022
95aeef2
1/3 of trivial fixes
mcdoll Dec 15, 2022
f0be7fa
s&r
mcdoll Dec 15, 2022
ef1369b
end of trivialities
mcdoll Dec 15, 2022
a3ab0d9
more trivialities
mcdoll Dec 15, 2022
87d6e68
fix
mcdoll Dec 15, 2022
ef1abd7
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 15, 2022
e034a83
port until 256
winstonyin Dec 15, 2022
7853e65
port until 793
winstonyin Dec 15, 2022
d033a37
port until 1595
winstonyin Dec 15, 2022
f5a8a51
compiles
winstonyin Dec 15, 2022
07a04dc
naming
winstonyin Dec 15, 2022
e40d173
long lines
winstonyin Dec 15, 2022
56cf268
progress
riccardobrasca Dec 15, 2022
26fc200
more progress
riccardobrasca Dec 15, 2022
8a6749e
minor improvements
ChrisHughes24 Dec 15, 2022
b82467a
shorten proof
ChrisHughes24 Dec 15, 2022
8dd1378
is_lub to isLUB in lemma names
ChrisHughes24 Dec 15, 2022
d3a615c
more is_lub
ChrisHughes24 Dec 15, 2022
1db63ff
Merge remote-tracking branch 'origin/mcdoll/order_bounds_basic' into …
riccardobrasca Dec 15, 2022
2b7c059
little progress
riccardobrasca Dec 15, 2022
bbd7f62
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 15, 2022
8bcd35d
why is it there?
riccardobrasca Dec 15, 2022
78fecde
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 19, 2022
78cf8af
progress
riccardobrasca Dec 19, 2022
f436d5d
add source header
riccardobrasca Dec 19, 2022
ca9d426
comment tactic
riccardobrasca Dec 20, 2022
e8f9f05
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 20, 2022
b5c29c4
long line
riccardobrasca Dec 20, 2022
fca98b1
again long line
riccardobrasca Dec 20, 2022
bce9363
last long line
riccardobrasca Dec 20, 2022
bfd9dba
fix mathlib.lean
riccardobrasca Dec 20, 2022
0b037ae
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 21, 2022
4fd25fc
fix one linter error
riccardobrasca Dec 21, 2022
d05a254
placate unusedHavesSuffices linter
kbuzzard Dec 21, 2022
4b2020d
better names
riccardobrasca Dec 21, 2022
751e8fb
ops
riccardobrasca Dec 21, 2022
caea325
I am stupid
riccardobrasca Dec 21, 2022
060118b
Merge remote-tracking branch 'origin/master' into RB/int.gcd
riccardobrasca Dec 21, 2022
ffcf17d
fix build
riccardobrasca Dec 21, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ import Mathlib.Data.Int.CharZero
import Mathlib.Data.Int.Div
import Mathlib.Data.Int.Dvd.Basic
import Mathlib.Data.Int.Dvd.Pow
import Mathlib.Data.Int.Gcd
import Mathlib.Data.Int.LeastGreatest
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Int.Order.Lemmas
Expand Down