Mathlib Changelog
v4
Changelog
About
Github
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