Commit 2026-03-26 13:40 25eb1935

chore(Combinatorics/SimpleGraph): fix order diamonds (#37148) This PR fixes two diamonds in the order hierarchy of simple graphs.

• We deprecate IsSubgraph, which appeared in the LE instance but not the PartialOrder instance. It was already the case that ≤ notation was preferred, so there is no problem in removing it entirely.
• The instance for CompletelyDistribLattice had bad defeq properies. We make it implicit_reducible again.