Compfiles/Imo2012P4.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2012, Problem 4

Determine all functions f : ℤ → ℤ such that for all integers a,b,c with a + b + c = 0, the following equality holds: f(a)² + f(b)² + f(c)² = 2f(a)f(b) + 2f(b)f(c) + 2f(c)f(a).

Imports (2)
Imported by 1 file
  1. def Imo2012P4.odd_const line 29 source

    standard axioms: propext what this means

    Statement uses: Set, Int

    Proof uses: Exists, And, Odd, Eq, Even, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. def Imo2012P4.mod4_cycle line 33 source

    no axioms what this means

    Statement uses: Set, Int

    Proof uses: Exists, Eq, Imo2012P4.mod4_cycle.match_1, HMod.hMod, OfNat.ofNat, Unit, HMul.hMul

    5 instances, coercions and auxiliary constants left out.

  3. def Imo2012P4.square_set line 40 source

    standard axioms: propext what this means

    Statement uses: Set, Int

    Proof uses: Exists, Eq, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

  4. theorem Imo2012P4.sub_sq'' line 43 source

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

    Statement uses: Int, Iff, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    Proof uses: Eq.mpr, HSub.hSub, id, congrArg, Eq.symm, propext, sub_eq_zero, sub_sq', sq_eq_zero_iff, Iff.rfl

    55 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  5. theorem Imo2012P4.myInduction line 46 source

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

    Statement uses: Int, OfNat.ofNat, Eq, HAdd.hAdd

    Proof uses: HMul.hMul, Int.induction_on, Eq.mpr, id, congrArg, Eq.trans, MulZeroClass.mul_zero, add_zero, Nat, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, HPow.hPow, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 41 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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

  6. determine Imo2012P4.solution_set line 76 source

    standard axioms: propext what this means

    Statement uses: Set, Int

    Proof uses: Union.union, Imo2012P4.odd_const, Imo2012P4.mod4_cycle, Imo2012P4.square_set

    1 instances, coercions and auxiliary constants left out.

  7. problem Imo2012P4.imo2012_p4 line 78 source

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

    Statement uses: Int, Iff, Membership.mem, Set, Imo2012P4.solution_set, Eq, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Nat, HMul.hMul

    Proof uses: Iff.intro, Union.union, Imo2012P4.odd_const, Imo2012P4.mod4_cycle, Imo2012P4.square_set, Neg.neg, And, Odd, Even, Or, Int.even_or_odd, Eq.mpr, id, congrArg, Eq.symm, propext, even_neg, neg_neg, Even.add, of_eq_true and 185 more

    214 instances, coercions and auxiliary constants left out.

    Tactic trace: 250 steps (first 200 of 250)

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