Strong product of two graphs

Stream: Is there code for X?

[Oliver Nash]

Am I right in thinking we do not have the strong product of two graphs anywhere?

(Other than this old Lean 3 repo: https://github.com/ocfnash/lean-shannon-lovasz/blob/master/src/to_mathlib/combinatorics/simple_graph/strong_product.lean)

[Yaël Dillies]

No, we do not have it

[Bhavik Mehta]

(and we should!)