Commit 2023-07-03 17:59 db9fb240

View on Github →

feat: port Archive.Imo.Imo1998Q2 (#5157)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo1998Q2.lean

added def Imo1998Q2.A

added theorem Imo1998Q2.A_card_lower_bound

added theorem Imo1998Q2.A_card_upper_bound

added theorem Imo1998Q2.A_fibre_over_contestant

added theorem Imo1998Q2.A_fibre_over_contestant_card

added theorem Imo1998Q2.A_fibre_over_judgePair

added theorem Imo1998Q2.A_fibre_over_judgePair_card

added theorem Imo1998Q2.A_maps_to_offDiag_judgePair

added theorem Imo1998Q2.JudgePair.agree_iff_same_rating

added theorem Imo1998Q2.add_sq_add_sq_sub

added def Imo1998Q2.agreedContestants

added theorem Imo1998Q2.clear_denominators

added theorem Imo1998Q2.distinct_judge_pairs_card_lower_bound

added theorem Imo1998Q2.judge_pairs_card_lower_bound

added theorem Imo1998Q2.norm_bound_of_odd_sum

added theorem imo1998_q2