Compfiles: Catalog Of Math Problems Formalized In Lean

Usa2013P5

module

public import Mathlib.Algebra.Order.Ring.Star
public import Mathlib.Data.Nat.Digits.Defs
public import Mathlib.Data.Nat.Factorization.Basic
public import Mathlib.Data.ZMod.Units
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.NormNum.GCD
public import Mathlib.Tactic.NormNum.Prime
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 2013, Problem 5

Given positive integers m and n, prove that there is a positive integer c
such that the numbers cm and cn have the same number of occurrences of each
non-zero digit when written in base ten.
-/

namespace Usa2013P5

theorem usa2013_p5 (m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
    ∃ c : ℕ, 0 < c ∧ ∀ d ∈ Finset.Icc 1 9,
      (Nat.digits 10 (c * m)).count d = (Nat.digits 10 (c * n)).count d := sorry

end Usa2013P5

File author(s): Kimi K3

This problem has a complete formalized solution.