mathlib

418373e8 - feat(combinatorics/simple_graph/basic): `dart.to_prod` is injective (#15150)