feat(Combinatorics/SimpleGraph/Bipartite): upper bound on the number of edges of a bipartite graph#34315
Open
LessnessRandomness wants to merge 17 commits intoleanprover-community:masterfrom
Commits
Commits on Jan 23, 2026
Commits on Jan 24, 2026
Commits on Jan 25, 2026
Changed proof to Vlad Tsyrklevich's proof and also added IsBipartite.four_mul_encard_edgeSet_le back
committed- committed
- committed
- committed