Compfiles/Imo1999P6.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1999, Problem 6

Determine all functions f : ℝ → ℝ such that

f(x - f(y)) = f(f(y)) + xf(y) + f(x) - 1

for all x,y ∈ ℝ.

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

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

    Statement uses: Set, Real

    Proof uses: Singleton.singleton, HSub.hSub, OfNat.ofNat, HDiv.hDiv, HPow.hPow, Nat

    16 instances, coercions and auxiliary constants left out.

  2. problem Imo1999P6.imo1999_p6 line 31 source

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

    Statement uses: Real, Iff, Membership.mem, Set, Imo1999P6.SolutionSet, Eq, HSub.hSub, HAdd.hAdd, HMul.hMul, OfNat.ofNat

    Proof uses: Eq.mpr, HDiv.hDiv, HPow.hPow, Nat, id, congrArg, Singleton.singleton, propext, Set.mem_singleton_iff, Iff.intro, inferInstance, GroupWithZero, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, Neg.neg, List.nil and 160 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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