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

[Merged by Bors] - feat: The Ahlswede-Zhang identity #8171

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat: The Ahlswede-Zhang identity #8171

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
433ea7c
feat: The Ahlswede-Zhang identity
YaelDillies Nov 3, 2023
cb4046b
break long line
YaelDillies Nov 3, 2023
fdcc98d
typo
YaelDillies Nov 10, 2023
fc9a493
explicit n
YaelDillies Nov 14, 2023
02d0884
Merge remote-tracking branch 'origin/master' into ahlswede_zhang
YaelDillies Dec 10, 2023
2aadff0
ugh
YaelDillies Dec 10, 2023
f4c914b
Merge remote-tracking branch 'origin/master' into ahlswede_zhang
YaelDillies Dec 19, 2023
67f21cf
rewrap
YaelDillies Dec 19, 2023
40fe9c8
fix module doc
YaelDillies Jan 8, 2024
e423472
fix module doc
YaelDillies Jan 8, 2024
78af6ba
Merge remote-tracking branch 'origin/master' into ahlswede_zhang
YaelDillies Jan 9, 2024
cd4e6c2
fix
YaelDillies Jan 9, 2024
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
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 @@ -1328,6 +1328,7 @@ import Mathlib.Combinatorics.Quiver.Push
import Mathlib.Combinatorics.Quiver.SingleObj
import Mathlib.Combinatorics.Quiver.Subquiver
import Mathlib.Combinatorics.Quiver.Symmetric
import Mathlib.Combinatorics.SetFamily.AhlswedeZhang
import Mathlib.Combinatorics.SetFamily.CauchyDavenport
import Mathlib.Combinatorics.SetFamily.Compression.Down
import Mathlib.Combinatorics.SetFamily.Compression.UV
Expand Down
Loading