Theorem SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two

Modification history

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.exists_isFiveWheelLike_succ_of_not_adj_le_twoView on Github →