Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-13 03:48 505b969c

View on Github →

feat(archive/imo): formalize IMO 1962 problem Q1 (#4450) The problem statement: Find the smallest natural number $n$ which has the following properties: (a) Its decimal representation has 6 as the last digit. (b) If the last digit 6 is erased and placed in front of the remaining digits, the resulting number is four times as large as the original number $n$. This is a proof that 153846 is the smallest member of the set satisfying these conditions.

Estimated changes

added theorem case_0_digit
added theorem case_1_digit
added theorem case_2_digit
added theorem case_3_digit
added theorem case_4_digit
added theorem case_5_digit
added theorem case_more_digits
added theorem helper_5_digit
added theorem imo1962_q1
added theorem no_smaller_solutions
added theorem satisfied_by_153846
added theorem without_digits