Commit 2025-04-09 03:56 b632aab9

View on Github →

feat: IMO 2015 Q6 (#23038)

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2015Q6.lean

added def Imo2015Q6.Condition

added theorem Imo2015Q6.b_pos

added theorem Imo2015Q6.card_pool_succ

added theorem Imo2015Q6.exists_add_eq_of_mem_pool

added theorem Imo2015Q6.exists_max_card_pool

added theorem Imo2015Q6.le_sum_pool

added theorem Imo2015Q6.monotone_card_pool

added theorem Imo2015Q6.not_mem_pool_self

added def Imo2015Q6.pool

added theorem Imo2015Q6.pool_subset_Icc

added theorem Imo2015Q6.result

added theorem Imo2015Q6.sum_pool_le

added theorem Imo2015Q6.sum_sub_sum_eq_sub

added theorem Imo2015Q6.sum_telescope

added theorem Imo2015Q6.zero_mem_pool

Modified Mathlib.lean

Modified Mathlib/Algebra/BigOperators/Intervals.lean

added theorem Finset.prod_Ico_div

Created Mathlib/Algebra/Order/Group/Int/Sum.lean

added theorem Finset.sum_Ico_le_sum

added theorem Finset.sum_le_sum_Ioc

added theorem Finset.sum_le_sum_range

added theorem Finset.sum_range_le_sum

Modified Mathlib/Order/Monotone/Basic.lean

added theorem converges_of_monotone_of_bounded