Circulant

📁 Source: Mathlib/Combinatorics/SimpleGraph/Circulant.lean

Statistics

Metric	Count
Definitions `circulantGraph`, `cycleGraph`, `cycle`, `cycleGraph_EulerianCircuit`, `instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet`, `instDecidableRelFinAdjCycleGraph`	6
Theorems `circulantGraph_adj`, `circulantGraph_adj_translate`, `circulantGraph_eq_erase_zero`, `circulantGraph_eq_symm`, `length_cycle`, `cycleGraph_EulerianCircuit_length`, `cycleGraph_adj`, `cycleGraph_adj'`, `cycleGraph_connected`, `cycleGraph_degree_three_le`, `cycleGraph_degree_two_le`, `cycleGraph_neighborFinset`, `cycleGraph_neighborSet`, `cycleGraph_one_adj`, `cycleGraph_one_eq_bot`, `cycleGraph_one_eq_top`, `cycleGraph_preconnected`, `cycleGraph_three_eq_top`, `cycleGraph_two_eq_top`, `cycleGraph_zero_adj`, `cycleGraph_zero_eq_bot`, `cycleGraph_zero_eq_top`, `pathGraph_le_cycleGraph`	23
Total	29

SimpleGraph

Definitions

Name	Category	Theorems
`circulantGraph` 📖	CompOp	4 math math: `circulantGraph_eq_symm`, `circulantGraph_eq_erase_zero`, `circulantGraph_adj_translate`, `circulantGraph_adj`
`cycleGraph` 📖	CompOp	21 math math: `chromaticNumber_cycleGraph_of_even`, `cycleGraph_adj'`, `cycleGraph_one_eq_bot`, `cycleGraph_two_eq_top`, `cycleGraph_three_eq_top`, `cycleGraph_degree_three_le`, `cycleGraph_connected`, `chromaticNumber_cycleGraph_of_odd`, `cycleGraph_neighborFinset`, `cycleGraph_adj`, `cycleGraph_one_eq_top`, `cycleGraph_one_adj`, `cycleGraph.length_cycle`, `cycleGraph_EulerianCircuit_length`, `cycleGraph_neighborSet`, `pathGraph_le_cycleGraph`, `cycleGraph_zero_adj`, `cycleGraph_degree_two_le`, `cycleGraph_preconnected`, `cycleGraph_zero_eq_bot`, `cycleGraph_zero_eq_top`
`cycleGraph_EulerianCircuit` 📖	CompOp	—
`instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet` 📖	CompOp	—
`instDecidableRelFinAdjCycleGraph` 📖	CompOp	3 math math: `cycleGraph_degree_three_le`, `cycleGraph_neighborFinset`, `cycleGraph_degree_two_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circulantGraph_adj` 📖	mathematical	—	`Adj` `circulantGraph` `Set` `Set.instMembership` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid`	—	—
`circulantGraph_adj_translate` 📖	mathematical	—	`Adj` `circulantGraph` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`AddRightCancelSemigroup.toIsRightCancelAdd` `add_sub_add_right_eq_sub`
`circulantGraph_eq_erase_zero` 📖	mathematical	—	`circulantGraph` `Set` `Set.instSDiff` `Set.instSingletonSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`ext` `sub_ne_zero_of_ne`
`circulantGraph_eq_symm` 📖	mathematical	—	`circulantGraph` `Set` `Set.instUnion` `InvolutiveNeg.toNeg` `Set.involutiveNeg` `SubtractionMonoid.toInvolutiveNeg` `AddGroup.toSubtractionMonoid`	—	`ext` `neg_sub`
`cycleGraph_EulerianCircuit_length` 📖	mathematical	—	`Walk.length` `cycleGraph` `cycleGraph.cycle`	—	`cycleGraph.length_cycle`
`cycleGraph_adj` 📖	mathematical	—	`Adj` `cycleGraph`	—	`sub_self` `Fin.instNeZeroHAddNatOfNat_mathlib`
`cycleGraph_adj'` 📖	mathematical	—	`Adj` `cycleGraph`	—	—
`cycleGraph_connected` 📖	mathematical	—	`Connected` `cycleGraph`	—	`Connected.mono` `pathGraph_le_cycleGraph` `pathGraph_connected`
`cycleGraph_degree_three_le` 📖	mathematical	—	`degree` `cycleGraph` `neighborSetFintype` `Fin.fintype` `instDecidableRelFinAdjCycleGraph`	—	`cycleGraph_degree_two_le` `Finset.card_pair` `add_assoc` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `instLawfulBCmpCompare_mathlib`
`cycleGraph_degree_two_le` 📖	mathematical	—	`degree` `cycleGraph` `neighborSetFintype` `Fin.fintype` `instDecidableRelFinAdjCycleGraph` `Finset.card` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`degree.eq_1` `cycleGraph_neighborFinset`
`cycleGraph_neighborFinset` 📖	mathematical	—	`neighborFinset` `cycleGraph` `neighborSetFintype` `Fin.fintype` `instDecidableRelFinAdjCycleGraph` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`Set.toFinset_congr` `cycleGraph_neighborSet` `Set.toFinset_insert` `Set.toFinset_singleton`
`cycleGraph_neighborSet` 📖	mathematical	—	`neighborSet` `cycleGraph` `Set` `Set.instInsert` `Set.instSingletonSet`	—	`Set.ext` `cycleGraph_adj` `sub_eq_iff_eq_add'` `eq_sub_iff_add_eq`
`cycleGraph_one_adj` 📖	mathematical	—	`Adj` `cycleGraph`	—	`cycleGraph_one_eq_bot`
`cycleGraph_one_eq_bot` 📖	mathematical	—	`cycleGraph` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Unique.instSubsingleton`
`cycleGraph_one_eq_top` 📖	mathematical	—	`cycleGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Unique.instSubsingleton`
`cycleGraph_preconnected` 📖	mathematical	—	`Preconnected` `cycleGraph`	—	`Preconnected.mono` `pathGraph_le_cycleGraph` `pathGraph_preconnected`
`cycleGraph_three_eq_top` 📖	mathematical	—	`cycleGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`cycleGraph_two_eq_top` 📖	mathematical	—	`cycleGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`cycleGraph_zero_adj` 📖	mathematical	—	`Adj` `cycleGraph`	—	—
`cycleGraph_zero_eq_bot` 📖	mathematical	—	`cycleGraph` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Unique.instSubsingleton`
`cycleGraph_zero_eq_top` 📖	mathematical	—	`cycleGraph` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`Unique.instSubsingleton`
`pathGraph_le_cycleGraph` 📖	mathematical	—	`SimpleGraph` `instLE` `pathGraph` `cycleGraph`	—	`Unique.instSubsingleton` `cycleGraph_adj'` `pathGraph_adj` `LT.lt.le` `Eq.le`

SimpleGraph.cycleGraph

Definitions

Name	Category	Theorems
`cycle` 📖	CompOp	2 math math: `length_cycle`, `SimpleGraph.cycleGraph_EulerianCircuit_length`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_cycle` 📖	mathematical	—	`SimpleGraph.Walk.length` `SimpleGraph.cycleGraph` `cycle`	—	—

---

← Back to Index