Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-08 11:29 93be74b1

View on Github →

feat(combinatorics/simple_graph/prod): Box product (#14867) Define simple_graph.box_prod, the box product of simple graphs. Show that it's commutative and associative, and prove its connectivity properties.

Estimated changes