Commit 2025-12-20 12:59 e9a7156e

View on Github →

feat: 2025 imo problem3 (#27254)

depends on: #28788
depends on: #28790
depends on: #28829

Estimated changes

Modified Archive.lean

Created Archive/Imo/Imo2025Q3.lean

added theorem Imo2025Q3.IsBonza.apply_dvd_pow

added theorem Imo2025Q3.IsBonza.apply_prime_eq_one_or_dvd_self_sub_apply

added theorem Imo2025Q3.IsBonza.apply_prime_gt_two_eq_one

added theorem Imo2025Q3.IsBonza.not_id_apply_prime_of_gt_eq_one

added theorem Imo2025Q3.IsBonza.not_id_two_pow

added def Imo2025Q3.IsBonza

added theorem Imo2025Q3.fExample.apply_le

added theorem Imo2025Q3.fExample.dvd_pow_sub

added theorem Imo2025Q3.fExample.isBonza

added def Imo2025Q3.fExample

added theorem Imo2025Q3.result

Modified Mathlib/Algebra/Ring/Int/Parity.lean

added theorem Int.coe_nat_two_pow_pred

added theorem Int.natCast_pow_pred

Modified Mathlib/NumberTheory/LucasLehmer.lean

deleted theorem LucasLehmer.Int.coe_nat_two_pow_pred

deleted theorem LucasLehmer.Int.natCast_pow_pred

Modified Mathlib/NumberTheory/Multiplicity.lean

added theorem padicValNat.pow_two_sub_one

added theorem padicValNat.pow_two_sub_one_ge

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

added theorem padicValNat_add_le_self