Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-10 18:48 0e014ba5

View on Github →

feat(combinatorics/simple_graph/adj_matrix): more lemmas (#9021)

Estimated changes

Modified src/combinatorics/simple_graph/adj_matrix.lean

added def matrix.compl

added theorem matrix.compl_apply

added theorem matrix.compl_apply_diag

added theorem matrix.is_adj_matrix.adj_matrix_to_graph_eq

added theorem matrix.is_adj_matrix.apply_diag_ne

added theorem matrix.is_adj_matrix.apply_ne_one_iff

added theorem matrix.is_adj_matrix.apply_ne_zero_iff

added theorem matrix.is_adj_matrix.compl

added def matrix.is_adj_matrix.to_graph

added theorem matrix.is_adj_matrix.to_graph_compl_eq

added structure matrix.is_adj_matrix

added theorem matrix.is_adj_matrix_compl

added theorem matrix.is_symm_compl

modified def simple_graph.adj_matrix

modified theorem simple_graph.adj_matrix_apply

modified theorem simple_graph.adj_matrix_dot_product

modified theorem simple_graph.adj_matrix_mul_apply

modified theorem simple_graph.adj_matrix_mul_self_apply_self

modified theorem simple_graph.adj_matrix_mul_vec_apply

modified theorem simple_graph.adj_matrix_mul_vec_const_apply

modified theorem simple_graph.adj_matrix_mul_vec_const_apply_of_regular

modified theorem simple_graph.adj_matrix_vec_mul_apply

modified theorem simple_graph.dot_product_adj_matrix

added theorem simple_graph.is_adj_matrix_adj_matrix

added theorem simple_graph.is_symm_adj_matrix

modified theorem simple_graph.mul_adj_matrix_apply

added theorem simple_graph.to_graph_adj_matrix_eq

modified theorem simple_graph.trace_adj_matrix

modified theorem simple_graph.transpose_adj_matrix