Theorem SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ

Modification history

2025-11-19 18:07
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
chore: clean up FiveWheelLike (#31813) …
Added SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succView on Github →
2025-11-18 10:56
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
chore: bump toolchain to v4.26.0-rc1 (#31763)
Deleted SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succView on Github →
2025-09-01 17:39
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
feat(SimpleGraph/FiveWheelLike): add the Andrásfai-Erdős-Sós theorem (#25836) …
Added SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succView on Github →