Commit 2020-08-27 14:44 6b556cf1

View on Github →

feat(combinatorics/adjacency_matrix): defines adjacency matrices of simple graphs (#3672) defines the adjacency matrix of a simple graph proves lemmas about adjacency matrix that will form the bulk of the proof of the friendship theorem (freek 83)

Estimated changes

Created src/combinatorics/adj_matrix.lean

added def simple_graph.adj_matrix

added theorem simple_graph.adj_matrix_apply

added theorem simple_graph.adj_matrix_dot_product

added theorem simple_graph.adj_matrix_mul_apply

added theorem simple_graph.adj_matrix_mul_self_apply_self

added theorem simple_graph.adj_matrix_mul_vec_apply

added theorem simple_graph.adj_matrix_mul_vec_const_apply

added theorem simple_graph.adj_matrix_mul_vec_const_apply_of_regular

added theorem simple_graph.adj_matrix_vec_mul_apply

added theorem simple_graph.dot_product_adj_matrix

added theorem simple_graph.mul_adj_matrix_apply

added theorem simple_graph.trace_adj_matrix

added theorem simple_graph.transpose_adj_matrix