Commit 2025-05-10 14:48 42e558f9

View on Github →

refactor(SimpleGraph): make completeGraph and emptyGraph abbrevs for ⊤ and ⊥ (#23838) define Top and Bot in-line for SimpleGraph and set completeGraph and emptyGraph as abbrev

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

deleted def completeGraph

deleted def emptyGraph

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

modified theorem SimpleGraph.cliqueFree_iff

modified theorem SimpleGraph.not_cliqueFree_iff

Modified Mathlib/Combinatorics/SimpleGraph/Coloring.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Combinatorics/SimpleGraph/Maps.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

modified def SimpleGraph.Subgraph.botEquiv

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