Commit 2021-01-29 11:30 41decdb1

View on Github →

chore(combinatorics/simple_graph/basic): remove classical locale (#5951) This completes the simple graph part of the refactor that removed classical fintype instances.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

modified theorem simple_graph.adj.card_common_neighbors_lt_degree

modified theorem simple_graph.card_common_neighbors_le_degree_left

modified theorem simple_graph.card_common_neighbors_le_degree_right

modified theorem simple_graph.card_common_neighbors_lt_card_verts

modified theorem simple_graph.degree_lt_card_verts