Commit 2024-07-24 10:59 82a3b223

View on Github →

feat(Archive/Imo): IMO 2024 Q2 (#14920) Formalize IMO 2024 Q2.

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2024Q2.lean

added theorem Imo2024Q2.Condition.N_le_large_n

added theorem Imo2024Q2.Condition.N_le_large_n_0

added theorem Imo2024Q2.Condition.N_pos

added theorem Imo2024Q2.Condition.N_spec

added theorem Imo2024Q2.Condition.a_coprime_ab_add_one

added theorem Imo2024Q2.Condition.a_eq_one

added theorem Imo2024Q2.Condition.a_pos

added theorem Imo2024Q2.Condition.ab_add_one_dvd_a_pow_large_n_0_add_b

added theorem Imo2024Q2.Condition.ab_add_one_dvd_a_pow_large_n_add_b

added theorem Imo2024Q2.Condition.ab_add_one_dvd_b_add_one

added theorem Imo2024Q2.Condition.ab_add_one_dvd_b_pow_large_n_add_a

added theorem Imo2024Q2.Condition.ab_add_one_dvd_g

added theorem Imo2024Q2.Condition.b_eq_one

added theorem Imo2024Q2.Condition.b_pos

added theorem Imo2024Q2.Condition.dvd_g_of_le_N_of_dvd

added theorem Imo2024Q2.Condition.dvd_large_n_0_sub_zero

added theorem Imo2024Q2.Condition.dvd_large_n_sub_neg_one

added theorem Imo2024Q2.Condition.g_pos

added theorem Imo2024Q2.Condition.g_spec

added theorem Imo2024Q2.Condition.gcd_eq_g

added theorem Imo2024Q2.Condition.symm_large_n

added theorem Imo2024Q2.Condition.symm_large_n_0

added def Imo2024Q2.Condition

added theorem Imo2024Q2.dvd_pow_iff_of_dvd_sub

added theorem Imo2024Q2.result

added def Imo2024Q2.solutionSet