Commit 2025-11-26 11:32 2aff67dc

View on Github →

refactor: redefine IsTuranMaximal (#28719) Redefined IsTuranMaximal := G.IsExtremal (CliqueFree · (r + 1)) and

replaced classical in IsTuranMaximal.le_iff_eq with DecidableRel
refactored turanGraph.instDecidableRelAdj, turanGraph_zero, exists_isTuranMaximal
added open Fintype
replaced simp only with rw or simp_rw

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean

added theorem SimpleGraph.IsExtremal.le_iff_eq

Modified Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean

modified theorem SimpleGraph.IsTuranMaximal.card_parts

deleted theorem SimpleGraph.IsTuranMaximal.le_iff_eq

modified def SimpleGraph.IsTuranMaximal

modified theorem SimpleGraph.not_cliqueFree_of_isTuranMaximal

modified theorem SimpleGraph.turanGraph_zero