Commit 2024-08-06 08:16 c63fd8a8

View on Github →

feat(Combinatorics/SimpleGraph): Add definition of circulant graph and cycle graph (#15501)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/SimpleGraph/Circulant.lean

added def SimpleGraph.circulantGraph

added theorem SimpleGraph.circulantGraph_adj_translate

added theorem SimpleGraph.circulantGraph_eq_erase_zero

added theorem SimpleGraph.circulantGraph_eq_symm

added def SimpleGraph.cycleGraph

added theorem SimpleGraph.cycleGraph_adj'

added theorem SimpleGraph.cycleGraph_adj

added theorem SimpleGraph.cycleGraph_connected

added theorem SimpleGraph.cycleGraph_degree_three_le

added theorem SimpleGraph.cycleGraph_degree_two_le

added theorem SimpleGraph.cycleGraph_neighborFinset

added theorem SimpleGraph.cycleGraph_neighborSet

added theorem SimpleGraph.cycleGraph_one_adj

added theorem SimpleGraph.cycleGraph_one_eq_bot

added theorem SimpleGraph.cycleGraph_one_eq_top

added theorem SimpleGraph.cycleGraph_preconnected

added theorem SimpleGraph.cycleGraph_three_eq_top

added theorem SimpleGraph.cycleGraph_two_eq_top

added theorem SimpleGraph.cycleGraph_zero_adj

added theorem SimpleGraph.cycleGraph_zero_eq_bot

added theorem SimpleGraph.cycleGraph_zero_eq_top

added theorem SimpleGraph.pathGraph_le_cycleGraph