Commit 2025-10-09 01:02 0b0ba00f
View on Github →chore(SimpleGraph/Subgraph): remove duplicate def and fix names (#29690)
We previously had Subgraph.topEquiv and Subgraph.topIso for the graph isomorphism (⊤ : G.Subgraph).coe ≃g G.
Subgraph.topIso seems preferable as a name for this so this PR deprecates the other name.
Also rename and deprecate Subgraph.botEquiv to Subgraph.botIso.