Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-19 22:45 a249c9a4

View on Github →

feat(archive/imo): formalize IMO 1998 problem 2 (#4502)

Estimated changes

Created archive/imo/imo1998_q2.lean

added def A

added theorem A_card_lower_bound

added theorem A_card_upper_bound

added theorem A_fibre_over_contestant

added theorem A_fibre_over_contestant_card

added theorem A_fibre_over_judge_pair

added theorem A_fibre_over_judge_pair_card

added theorem A_maps_to_off_diag_judge_pair

added theorem add_sq_add_sq_sub

added def agreed_contestants

added def agreed_triple.contestant

added def agreed_triple.judge_pair

added def agreed_triple

added theorem clear_denominators

added theorem distinct_judge_pairs_card_lower_bound

added theorem imo1998_q2

added def judge_pair.agree

added theorem judge_pair.agree_iff_same_rating

added def judge_pair.distinct

added def judge_pair.judge₁

added def judge_pair.judge₂

added def judge_pair

added theorem judge_pairs_card_lower_bound

added theorem norm_bound_of_odd_sum

Modified src/data/finset/basic.lean

added def finset.diag

added theorem finset.diag_card

added theorem finset.filter_card_add_filter_neg_card_eq_card

added theorem finset.filter_product

added theorem finset.filter_product_card

added theorem finset.mem_diag

added theorem finset.mem_off_diag

added def finset.off_diag

added theorem finset.off_diag_card

Modified src/data/int/parity.lean

added theorem int.ne_of_odd_sum

Modified src/data/nat/parity.lean

added theorem nat.odd_gt_zero