Commit 2025-09-01 07:30 32cc84e5

feat: number of edges in the Turán graph (#25788) We provide two theorems, the first card_edgeFinset_turanGraph providing the exact number of edges and the other mul_card_edgeFinset_turanGraph_le providing a (slightly) looser bound whose main advantage is its lack of division/modulus operations. The bound in mul_card_edgeFinset_turanGraph_le is also the bound provided in Motzkin and Straus (1965).