Compfiles/Imo1996P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1996, Problem 3

Let S denote the set of nonnegative integers. Find all functions f from S to itself such that

f(m + f(n)) = f(f(m)) + f(n)

for all m,n in S.

Imports (2)
Imported by 1 file
  1. determine Imo1996P3.SolutionSet line 33 source

    no axioms what this means

    Statement uses: Set, Nat

    Proof uses: Set.ofPred, Exists, And, Eq, OfNat.ofNat, HAdd.hAdd, HMul.hMul, HDiv.hDiv, HMod.hMod

    9 instances, coercions and auxiliary constants left out.

  2. problem Imo1996P3.imo1996_p3 line 37 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Iff, Membership.mem, Set, Imo1996P3.SolutionSet, Eq, HAdd.hAdd

    Proof uses: Iff.intro, Exists, And, OfNat.ofNat, HMul.hMul, HDiv.hDiv, HMod.hMod, GT.gt, Or, Nat.eq_zero_or_pos, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, congrFun', Nat.div_zero, MulZeroClass.mul_zero and 66 more

    72 instances, coercions and auxiliary constants left out.

    Tactic trace: 108 steps

    Open to load the checked before-and-after goal states.