Mathlib Changelog
v3
Changelog
About
Github
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