Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 06:48 2688d42b

View on Github →

feat(archive/100-theorems-list): friendship theorem (nr 83) (#3970) defines friendship graphs proves the friendship theorem (freek #83)

Estimated changes

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

added def common_friends

added def exists_politician

added theorem friendship.adj_matrix_mul_const_one_mod_p_of_regular

added theorem friendship.adj_matrix_pow_mod_p_of_regular

added theorem friendship.adj_matrix_pow_three_of_not_adj

added theorem friendship.adj_matrix_sq_mod_p_of_regular

added theorem friendship.adj_matrix_sq_mul_const_one_of_regular

added theorem friendship.adj_matrix_sq_of_ne

added theorem friendship.adj_matrix_sq_of_regular

added theorem friendship.card_mod_p_of_regular

added theorem friendship.card_of_regular

added theorem friendship.degree_eq_of_not_adj

added theorem friendship.exists_politician_of_degree_eq_two

added theorem friendship.exists_politician_of_degree_le_one

added theorem friendship.exists_politician_of_degree_le_two

added theorem friendship.false_of_three_le_degree

added theorem friendship.is_regular_of_not_exists_politician

added theorem friendship.neighbor_finset_eq_of_degree_eq_two

added def friendship

added theorem friendship_theorem

added theorem mem_common_friends

Modified docs/references.bib