mathlib

93be74b1 - feat(combinatorics/simple_graph/prod): Box product (#14867)

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.