Compfiles/Imo2015P5.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2015, Problem 5

Determine all functions f : ℝ → ℝ that satisfy

f(x + f(x + y)) + f(xy) = x + f(x + y) + yf(x)

for all x,y.

Imports (2)
Imported by 1 file
  1. determine Imo2015P5.SolutionSet line 29 source

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

    Statement uses: Set, Real

    Proof uses: Insert.insert, Singleton.singleton, HSub.hSub, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

  2. problem Imo2015P5.imo2015_p5 line 31 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo2015P5.SolutionSet, Eq, HAdd.hAdd, HMul.hMul

    Proof uses: Iff.intro, Singleton.singleton, HSub.hSub, OfNat.ofNat, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt, Mathlib.Tactic.Ring.Common.add_pf_zero_add, Mathlib.Tactic.Ring.Common.add_pf_add_overlap, Mathlib.Tactic.Ring.Common.add_overlap_pf and 86 more

    122 instances, coercions and auxiliary constants left out.

    Tactic trace: 75 steps

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