Commit 2023-11-04 15:05 2fd9651c

View on Github →

chore: Fix name of SimpleGraph.Adj projection (#8179) simps was generating lemmas named _Adj. This PR makes it generate _adj instead, to follow the naming convention.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

Modified Mathlib/Combinatorics/SimpleGraph/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Clique.lean

Modified Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

deleted theorem SimpleGraph.Subgraph.coeSubgraph_Adj

added theorem SimpleGraph.Subgraph.coeSubgraph_adj

deleted theorem SimpleGraph.Subgraph.restrict_Adj

added theorem SimpleGraph.Subgraph.restrict_adj