Commit 2025-04-28 19:52 734b51c3

feat(Combinatorics/SimpleGraph): define extremalNumber (#19865) Define the extremal number extremalNumber n H of a natural number n and a simple graph H: extremalNumber n H is the maximum number of edges in a H-free simple graph on n vertices, if H is contained in all simple graphs on n vertices, then this is 0. Also define the predicate that a simple graph is an extremal graph IsExtremal satisfying some predicate.