Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-14 07:15 1509c295

View on Github →

chore(archive/100-theorems-list): 83_friendship_graphs (#5727) Cleaned up some lint and put it in terms of the new simple_graph.common_neighbors.

Estimated changes

Modified archive/100-theorems-list/83_friendship_graphs.lean

deleted def common_friends

modified theorem friendship.adj_matrix_pow_mod_p_of_regular

modified theorem friendship.false_of_three_le_degree

modified def friendship

modified theorem friendship_theorem

deleted theorem mem_common_friends

Modified src/combinatorics/simple_graph/basic.lean

added theorem simple_graph.mem_common_neighbors