Commit 2024-06-26 14:44 0c8452ec

View on Github →

feat: Turán's theorem (#9317)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Turan.lean

modified theorem SimpleGraph.IsTuranMaximal.equivalence_not_adj

added theorem SimpleGraph.IsTuranMaximal.iso

modified theorem SimpleGraph.IsTuranMaximal.not_adj_trans

added theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph

added theorem SimpleGraph.isTuranMaximal_of_iso

modified theorem SimpleGraph.isTuranMaximal_turanGraph