Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 20:48 0cfae438

View on Github →

feat(archive/imo): IMO 2021 Q1 (#8432) Formalised solution to IMO 2021 Q1

Estimated changes

Created archive/imo/imo2021_q1.lean

added theorem IMO_2021_Q1

added theorem exists_finset_3_le_card_with_pairs_summing_to_squares

added theorem exists_numbers_in_interval

added theorem exists_triplet_summing_to_squares

added theorem lower_bound

added theorem radical_inequality

added theorem upper_bound

Modified src/algebra/order/monoid.lean

added theorem lt_or_lt_of_add_lt_add

Modified src/data/finset/basic.lean

added theorem finset.exists_subset_or_subset_of_two_mul_lt_card