Commit 2024-07-20 16:12 e45b708c

View on Github →

feat(Archive/Imo): IMO 2024 Q6 (#14842) Formalize IMO 2024 Q6.

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2024Q6.lean

added theorem Imo2024Q6.Aquaesulian.card_le_two

added def Imo2024Q6.Aquaesulian

added theorem Imo2024Q6.General.Aquaesulian.apply_apply_add

added theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply

added theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_add

added theorem Imo2024Q6.General.Aquaesulian.apply_neg_apply_neg

added theorem Imo2024Q6.General.Aquaesulian.apply_neg_eq_neg_iff

added theorem Imo2024Q6.General.Aquaesulian.apply_neg_of_apply_eq

added theorem Imo2024Q6.General.Aquaesulian.apply_zero

added theorem Imo2024Q6.General.Aquaesulian.card_le_two

added theorem Imo2024Q6.General.Aquaesulian.eq_of_apply_eq_inl

added theorem Imo2024Q6.General.Aquaesulian.g_two

added theorem Imo2024Q6.General.Aquaesulian.injective

added theorem Imo2024Q6.General.Aquaesulian.pair_lemma

added theorem Imo2024Q6.General.Aquaesulian.u_eq_zero

added theorem Imo2024Q6.General.Aquaesulian.u_eq_zero_or_v_eq_zero

added def Imo2024Q6.General.Aquaesulian

added theorem Imo2024Q6.add_fExample

added theorem Imo2024Q6.apply_fExample_add_apply_of_fract_le

added theorem Imo2024Q6.aquaesulian_fExample

added theorem Imo2024Q6.aquaesulian_iff_general

added theorem Imo2024Q6.card_range_fExample

added def Imo2024Q6.fExample

added theorem Imo2024Q6.fExample_add

added theorem Imo2024Q6.fExample_int_add

added theorem Imo2024Q6.fExample_of_mem_Ico

added theorem Imo2024Q6.floor_fExample

added theorem Imo2024Q6.fract_fExample

added theorem imo2024q6