Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `boxProdSumDistrib`, `sumBoxProdDistrib`, `boxProdLeft`, `boxProdRight`, `ofBoxProdLeft`, `ofBoxProdRight`, `boxProd`, `boxProdAssoc`, `boxProdComm`, `boxProdFintypeNeighborSet`, `boxProdLeft`, `boxProdRight`, `«term_□_»`	13
Theorems `boxProd`, `ofBoxProdLeft`, `ofBoxProdRight`, `boxProdSumDistrib_apply`, `boxProdSumDistrib_symm_apply`, `boxProdSumDistrib_toEquiv`, `sumBoxProdDistrib_apply`, `sumBoxProdDistrib_symm_apply`, `sumBoxProdDistrib_toEquiv`, `boxProd`, `ofBoxProdLeft`, `ofBoxProdRight`, `length_boxProd`, `ofBoxProdLeft_boxProdLeft`, `ofBoxProdRight_boxProdRight`, `boxProdAssoc_apply`, `boxProdAssoc_symm_apply`, `boxProdComm_apply`, `boxProdComm_symm_apply`, `boxProdLeft_apply`, `boxProdRight_apply`, `boxProd_adj`, `boxProd_adj_left`, `boxProd_adj_right`, `connected_boxProd`, `degree_boxProd`, `edist_boxProd`, `neighborFinset_boxProd`, `neighborSet_boxProd`, `reachable_boxProd`	30
Total	43

SimpleGraph

Definitions

Name	Category	Theorems
`boxProd` 📖	CompOp	25 math math: `boxProd_adj_right`, `Iso.sumBoxProdDistrib_apply`, `Connected.boxProd`, `hasse_prod`, `boxProd_adj_left`, `boxProdComm_symm_apply`, `neighborFinset_boxProd`, `boxProdAssoc_apply`, `Walk.length_boxProd`, `reachable_boxProd`, `Iso.boxProdSumDistrib_symm_apply`, `Iso.boxProdSumDistrib_apply`, `Iso.boxProdSumDistrib_toEquiv`, `boxProd_adj`, `boxProdAssoc_symm_apply`, `neighborSet_boxProd`, `Iso.sumBoxProdDistrib_symm_apply`, `boxProdRight_apply`, `edist_boxProd`, `Iso.sumBoxProdDistrib_toEquiv`, `Preconnected.boxProd`, `boxProdLeft_apply`, `degree_boxProd`, `boxProdComm_apply`, `connected_boxProd`
`boxProdAssoc` 📖	CompOp	2 math math: `boxProdAssoc_apply`, `boxProdAssoc_symm_apply`
`boxProdComm` 📖	CompOp	2 math math: `boxProdComm_symm_apply`, `boxProdComm_apply`
`boxProdFintypeNeighborSet` 📖	CompOp	—
`boxProdLeft` 📖	CompOp	1 math math: `boxProdLeft_apply`
`boxProdRight` 📖	CompOp	1 math math: `boxProdRight_apply`
`«term_□_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boxProdAssoc_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Adj` `boxProd` `RelIso.instFunLike` `boxProdAssoc`	—	—
`boxProdAssoc_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Adj` `boxProd` `RelIso.instFunLike` `RelIso.symm` `boxProdAssoc`	—	—
`boxProdComm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Adj` `boxProd` `RelIso.instFunLike` `boxProdComm`	—	—
`boxProdComm_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Adj` `boxProd` `RelIso.instFunLike` `RelIso.symm` `boxProdComm`	—	—
`boxProdLeft_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Adj` `boxProd` `RelEmbedding.instFunLike` `boxProdLeft`	—	—
`boxProdRight_apply` 📖	mathematical	—	`DFunLike.coe` `RelEmbedding` `Adj` `boxProd` `RelEmbedding.instFunLike` `boxProdRight`	—	—
`boxProd_adj` 📖	mathematical	—	`Adj` `boxProd`	—	—
`boxProd_adj_left` 📖	mathematical	—	`Adj` `boxProd`	—	—
`boxProd_adj_right` 📖	mathematical	—	`Adj` `boxProd`	—	—
`connected_boxProd` 📖	mathematical	—	`Connected` `boxProd`	—	`Connected.ofBoxProdLeft` `Connected.ofBoxProdRight` `Connected.boxProd`
`degree_boxProd` 📖	mathematical	—	`degree` `boxProd`	—	`degree.eq_1` `Finset.disjoint_product` `neighborFinset_disjoint_singleton` `neighborFinset_boxProd` `Finset.card_disjUnion` `Finset.card_product` `Finset.card_singleton` `mul_one` `one_mul`
`edist_boxProd` 📖	mathematical	—	`edist` `boxProd` `ENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`top_add` `add_top` `exists_walk_of_edist_ne_top` `Walk.length_append` `Walk.length_map` `le_antisymm` `edist_le` `Walk.length_boxProd` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add`
`neighborFinset_boxProd` 📖	mathematical	—	`neighborFinset` `boxProd` `Finset.disjUnion` `SProd.sprod` `Finset` `Finset.instSProd` `Finset.instSingleton` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finset.disjoint_product` `neighborFinset_disjoint_singleton`	—	`Finset.disjoint_product` `neighborFinset_disjoint_singleton` `Lean.Meta.FastSubsingleton.elim` `Fintype.instFastSubsingleton` `Equiv.bijective` `Finset.map_map` `Finset.attach_map_val`
`neighborSet_boxProd` 📖	mathematical	—	`neighborSet` `boxProd` `Set` `Set.instUnion` `SProd.sprod` `Set.instSProd` `Set.instSingletonSet`	—	`Set.ext`
`reachable_boxProd` 📖	mathematical	—	`Reachable` `boxProd`	—	—

SimpleGraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boxProd` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.boxProd`	—	`SimpleGraph.Preconnected.boxProd` `preconnected` `nonempty`
`ofBoxProdLeft` 📖	—	`SimpleGraph.Connected` `SimpleGraph.boxProd`	—	—	`SimpleGraph.Preconnected.ofBoxProdLeft` `nonempty_prod` `nonempty` `preconnected`
`ofBoxProdRight` 📖	—	`SimpleGraph.Connected` `SimpleGraph.boxProd`	—	—	`SimpleGraph.Preconnected.ofBoxProdRight` `nonempty_prod` `nonempty` `preconnected`

SimpleGraph.Iso

Definitions

Name	Category	Theorems
`boxProdSumDistrib` 📖	CompOp	3 math math: `boxProdSumDistrib_symm_apply`, `boxProdSumDistrib_apply`, `boxProdSumDistrib_toEquiv`
`sumBoxProdDistrib` 📖	CompOp	3 math math: `sumBoxProdDistrib_apply`, `sumBoxProdDistrib_symm_apply`, `sumBoxProdDistrib_toEquiv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boxProdSumDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.boxProd` `SimpleGraph.sum` `RelIso.instFunLike` `boxProdSumDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.sumProdDistrib`	—	—
`boxProdSumDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `SimpleGraph.boxProd` `RelIso.instFunLike` `RelIso.symm` `boxProdSumDistrib` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.sumProdDistrib`	—	—
`boxProdSumDistrib_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `SimpleGraph.Adj` `SimpleGraph.boxProd` `SimpleGraph.sum` `boxProdSumDistrib` `Equiv.prodSumDistrib`	—	—
`sumBoxProdDistrib_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.boxProd` `SimpleGraph.sum` `RelIso.instFunLike` `sumBoxProdDistrib`	—	—
`sumBoxProdDistrib_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `SimpleGraph.Adj` `SimpleGraph.sum` `SimpleGraph.boxProd` `RelIso.instFunLike` `RelIso.symm` `sumBoxProdDistrib`	—	—
`sumBoxProdDistrib_toEquiv` 📖	mathematical	—	`RelIso.toEquiv` `SimpleGraph.Adj` `SimpleGraph.boxProd` `SimpleGraph.sum` `sumBoxProdDistrib` `Equiv.sumProdDistrib`	—	—

SimpleGraph.Preconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`boxProd` 📖	mathematical	`SimpleGraph.Preconnected`	`SimpleGraph.boxProd`	—	—
`ofBoxProdLeft` 📖	—	`SimpleGraph.Preconnected` `SimpleGraph.boxProd`	—	—	—
`ofBoxProdRight` 📖	—	`SimpleGraph.Preconnected` `SimpleGraph.boxProd`	—	—	—

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`boxProdLeft` 📖	CompOp	1 math math: `ofBoxProdLeft_boxProdLeft`
`boxProdRight` 📖	CompOp	1 math math: `ofBoxProdRight_boxProdRight`
`ofBoxProdLeft` 📖	CompOp	2 math math: `length_boxProd`, `ofBoxProdLeft_boxProdLeft`
`ofBoxProdRight` 📖	CompOp	2 math math: `length_boxProd`, `ofBoxProdRight_boxProdRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`length_boxProd` 📖	mathematical	—	`length` `SimpleGraph.boxProd` `ofBoxProdLeft` `ofBoxProdRight`	—	—
`ofBoxProdLeft_boxProdLeft` 📖	mathematical	—	`ofBoxProdLeft` `boxProdLeft`	—	`boxProdLeft.eq_1` `SimpleGraph.Hom.map_adj` `map_cons` `ofBoxProdLeft.eq_2` `Or.by_cases.eq_1` `cons.congr_simp`
`ofBoxProdRight_boxProdRight` 📖	mathematical	—	`ofBoxProdRight` `boxProdRight`	—	`boxProdRight.eq_1` `SimpleGraph.Hom.map_adj` `map_cons` `ofBoxProdRight.eq_2` `Or.by_cases.eq_1` `cons.congr_simp`

---

← Back to Index