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

feat(combinatorics/set_family/kruskal_katona): The Kruskal-Katona theorem #2770

Closed
wants to merge 44 commits into from
Closed

feat(combinatorics/set_family/kruskal_katona): The Kruskal-Katona theorem #2770

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
92737ce
Add combinatorics
b-mehta Apr 15, 2020
bbdcf25
fixups
b-mehta Apr 20, 2020
fed84b3
more fixup
b-mehta Apr 20, 2020
b7da168
use classical instead of decidable
b-mehta Apr 20, 2020
c564826
fixup
b-mehta May 9, 2020
363561d
update mathlib
b-mehta May 21, 2020
c578f75
minor cleanups
b-mehta May 21, 2020
5fb81d4
Merge branch 'master' of https://github.com/leanprover-community/math…
agusakov Oct 22, 2020
1a1f6ec
fixed some stuff
agusakov Oct 22, 2020
c9f1a6f
colex and UV are good
agusakov Oct 22, 2020
89385fe
so many errors oh god
agusakov Oct 22, 2020
bf8c102
colex stuff is good
agusakov Oct 31, 2020
fc8a713
i don't even know what i did
agusakov Oct 31, 2020
4e37b9f
Merge branch 'master' of https://github.com/leanprover-community/math…
agusakov Oct 31, 2020
237c19d
SHADOWS DONE, FINALLY
agusakov Oct 31, 2020
6318228
Merge branch 'master' of https://github.com/leanprover-community/math…
agusakov Oct 31, 2020
0178cb2
colex broke again somehow?
agusakov Nov 1, 2020
a690c2d
gotta fix this swap
agusakov Nov 1, 2020
e2c9123
fixed
agusakov Nov 1, 2020
5fb06ed
Merge branch 'master' of https://github.com/leanprover-community/math…
agusakov Nov 1, 2020
b2aa390
style fixes
agusakov Nov 1, 2020
34eefbc
shadows.lean seems to be ready to go
agusakov Nov 1, 2020
69f624f
okay now it really looks ready
agusakov Nov 1, 2020
e05b466
basic.lean is ready to go
agusakov Nov 1, 2020
eec39ac
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Oct 19, 2021
b9d3182
fix
YaelDillies Oct 19, 2021
aaeb35c
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Oct 31, 2021
b21653d
bump mathlib
YaelDillies Oct 31, 2021
d162ef5
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Nov 17, 2021
8243e50
bump mathlib
YaelDillies Nov 17, 2021
c3e2f8d
move files to combinatorics.set_family
YaelDillies Nov 18, 2021
54f4089
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Dec 2, 2021
10d2137
kill all_removals
YaelDillies Dec 2, 2021
b275977
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Jan 4, 2022
92ec07b
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Mar 1, 2022
c0bd681
bump and golf
YaelDillies Mar 2, 2022
4ed9a0c
Merge branch 'master' into combinatorics
YaelDillies Jun 26, 2022
edf57a1
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies May 23, 2023
ac5d6bd
fix most of it
YaelDillies May 23, 2023
718b0b4
skip colex.partial_order
YaelDillies May 23, 2023
d8ac2fe
sorry-free again 🎉
YaelDillies May 24, 2023
413344e
todo
YaelDillies May 24, 2023
cf6fa92
break long line
YaelDillies Jun 1, 2023
23aaaaa
Merge remote-tracking branch 'origin/master' into combinatorics
YaelDillies Sep 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading