Documentation Verification Report

ConcreteColorings

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

Statistics

Metric	Count
Definitions `completeEquipartiteGraph`, `bicoloring_of_even`, `tricoloring`, `bicoloring`, `pathGraph_two_embedding`	5
Theorems `even_length_iff_congr`, `odd_length_iff_not_congr`, `three_le_chromaticNumber_of_odd_loop`, `chromaticNumber_cycleGraph_of_even`, `chromaticNumber_cycleGraph_of_odd`, `chromaticNumber_eq_two_iff`, `chromaticNumber_le_two_iff_isBipartite`, `chromaticNumber_pathGraph`, `completeEquipartiteGraph_colorable`, `two_colorable_iff_forall_loop_even`	10
Total	15

SimpleGraph

Definitions

Name	Category	Theorems
`pathGraph_two_embedding` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chromaticNumber_cycleGraph_of_even` 📖	mathematical	`Even`	`chromaticNumber` `cycleGraph` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Coloring.colorable` `le_antisymm` `Nat.instAtLeastTwoHAddOfNat` `Colorable.chromaticNumber_le` `Nat.instCanonicallyOrderedAdd` `tsub_zero` `Nat.instOrderedSub` `two_le_chromaticNumber_of_adj`
`chromaticNumber_cycleGraph_of_odd` 📖	mathematical	`Odd` `Nat.instSemiring`	`chromaticNumber` `cycleGraph` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Coloring.colorable` `le_antisymm` `Nat.instAtLeastTwoHAddOfNat` `Colorable.chromaticNumber_le` `Nat.not_odd_iff` `cycleGraph_EulerianCircuit_length` `Walk.three_le_chromaticNumber_of_odd_loop`
`chromaticNumber_eq_two_iff` 📖	mathematical	—	`chromaticNumber` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `IsBipartite`	—	`Nat.instAtLeastTwoHAddOfNat` `chromaticNumber_le_two_iff_isBipartite` `two_le_chromaticNumber_iff_ne_bot` `ENat.eq_of_forall_natCast_le_iff` `LE.le.trans`
`chromaticNumber_le_two_iff_isBipartite` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `chromaticNumber` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `IsBipartite`	—	`chromaticNumber_le_iff_colorable`
`chromaticNumber_pathGraph` 📖	mathematical	—	`chromaticNumber` `pathGraph` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Coloring.colorable` `le_antisymm` `Nat.instAtLeastTwoHAddOfNat` `Colorable.chromaticNumber_le` `zero_add` `Nat.instCharZero` `two_le_chromaticNumber_of_adj`
`completeEquipartiteGraph_colorable` 📖	mathematical	—	`Colorable` `completeEquipartiteGraph`	—	—
`two_colorable_iff_forall_loop_even` 📖	mathematical	—	`Colorable` `Even` `Walk.length`	—	`Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `Walk.three_le_chromaticNumber_of_odd_loop` `Colorable.chromaticNumber_le` `colorable_iff_forall_connectedComponents` `ConnectedComponent.nonempty_supp` `Connected.preconnected` `ConnectedComponent.connected_toSimpleGraph` `Walk.length_map` `Walk.length_append` `Walk.length_concat` `Walk.length_reverse` `add_right_comm` `Even.add_one` `Nat.even_iff`

SimpleGraph.Coloring

Definitions

Name	Category	Theorems
`completeEquipartiteGraph` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`even_length_iff_congr` 📖	mathematical	—	`Even` `SimpleGraph.Walk.length` `DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.completeGraph`	—	`not_iff` `valid`
`odd_length_iff_not_congr` 📖	mathematical	—	`Odd` `Nat.instSemiring` `SimpleGraph.Walk.length` `DFunLike.coe` `SimpleGraph.Coloring` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.completeGraph`	—	`Nat.not_even_iff_odd` `even_length_iff_congr`

SimpleGraph.Walk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`three_le_chromaticNumber_of_odd_loop` 📖	mathematical	`Odd` `Nat.instSemiring` `length`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `SimpleGraph.chromaticNumber`	—	`Classical.by_contradiction` `Nat.instAtLeastTwoHAddOfNat` `Order.le_of_lt_add_one` `not_le` `SimpleGraph.chromaticNumber_le_iff_colorable` `SimpleGraph.Coloring.odd_length_iff_not_congr`

SimpleGraph.cycleGraph

Definitions

Name	Category	Theorems
`bicoloring_of_even` 📖	CompOp	—
`tricoloring` 📖	CompOp	—

SimpleGraph.pathGraph

Definitions

Name	Category	Theorems
`bicoloring` 📖	CompOp	—

---

← Back to Index