Compfiles/Imo1975P6.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1975, Problem 6

Find all polynomials P, in two variables, with the following properties:

(i) for a positive integer n and all real t, x, y P(tx, ty) = tⁿP(x, y) (that is, P is homogeneous of degree n),

(ii) for all real a, b, c, P(b + c, a) + P(c + a, b) + P(a + b, c) = 0,

(iii) P(1, 0) = 1.

Imports (2)
Imported by 1 file
  1. determine Imo1975P6.solution_set line 37 source

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

    Statement uses: Set, Polynomial, Real

    Proof uses: Set.ofPred, Exists, Nat, Eq, HMul.hMul, HSub.hSub, RingHom, Polynomial.C, Polynomial.X, OfNat.ofNat, HPow.hPow, HAdd.hAdd

    22 instances, coercions and auxiliary constants left out.

  2. lemma Imo1975P6.mul_pow_eq_pow_succ line 41 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Real, Eq, HMul.hMul, HPow.hPow, HSub.hSub

    Proof uses: Eq.mpr, id, congrArg, Eq.symm, pow_mul_comm', HAdd.hAdd, pow_succ, Nat.succ, Nat.sub_add_cancel, Eq.refl

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. lemma Imo1975P6.eq_if_continuous_and_eq_almost_everywhere line 44 source

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

    Statement uses: Real, Continuous, Rat, Eq

    Proof uses: LE.le, Set, Set.range, Set.ofPred, Membership.mem, closure, Iff.mpr, IsClosed.closure_subset_iff, isClosed_eq, of_eq_true, Eq.trans, Set.univ, True, congrFun', congrArg, TopologicalSpace, Field, LinearOrder, IsStrictOrderedRing, OrderTopology and 3 more

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  4. lemma Imo1975P6.eq_if_continuous_and_eq_except_one_point line 50 source

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

    Statement uses: Real, Continuous, Ne, Eq

    Proof uses: Dense, Set.ofPred, Set, Compl.compl, Singleton.singleton, Set.ext, of_eq_true, Iff, Not, Membership.mem, Eq.trans, True, congrArg, iff_self, Eq.mpr, id, dense_compl_singleton, Continuous.ext_on

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  5. lemma Imo1975P6.eq_if_evalEval_eq line 58 source

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

    Statement uses: Polynomial, Real, Eq, Polynomial.evalEval

    Proof uses: Polynomial.eq_of_infinite_eval_eq, Set.Infinite.mono, Set.range, RingHom, Polynomial.C, Set.ofPred, Polynomial.eval, Membership.mem, Set, Polynomial.funext, Set.infinite_range_of_injective, Polynomial.C_injective

    28 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  6. lemma Imo1975P6.aux₁ line 65 source

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

    Statement uses: Nat, LT.lt, OfNat.ofNat, Ne, Real, HAdd.hAdd, HPow.hPow, HMul.hMul, Neg.neg

    Proof uses: Even, Odd, Or, Nat.even_or_odd, Eq, Eq.mpr, Not, id, congrFun', congrArg, Eq.trans, Even.neg_pow, of_eq_true, one_pow, mul_one, ne_of_gt, add_pos', pow_pos, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat and 30 more

    129 instances, coercions and auxiliary constants left out.

    Tactic trace: 10 steps

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

  7. lemma Imo1975P6.aux₂ line 74 source

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

    Statement uses: Real, Nat, Ne, OfNat.ofNat, Eq, HMul.hMul, HPow.hPow, Inv.inv

    Proof uses: Eq.mpr, id, congrArg, mul_assoc, mul_comm, of_eq_true, Eq.trans, True, congrFun', inv_pow, mul_inv_cancel₀, Not, False, And, eq_false, false_and, not_false_eq_true, mul_one, eq_self

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  8. lemma Imo1975P6.linear_int line 79 source

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

    Statement uses: Real, Eq, HAdd.hAdd, Int, HMul.hMul

    Proof uses: Int.induction_on, Nat, Eq.mpr, OfNat.ofNat, id, congr, congrArg, congrFun', Eq.trans, Int.cast_add, Int.cast_natCast, Int.cast_one, Eq.mp, forall_congr, Neg.neg, HSub.hSub, Int.cast_sub, Int.cast_neg, neg_mul

    49 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

  9. lemma Imo1975P6.linear_inv line 89 source

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

    Statement uses: Real, Int, Eq, HMul.hMul, HDiv.hDiv, OfNat.ofNat

    Proof uses: dite, Not

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  10. lemma Imo1975P6.linear_rat line 94 source

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

    Statement uses: Real, Int, Eq, HMul.hMul, Rat, OfNat.ofNat

    Proof uses: Rat.num, HDiv.hDiv, Rat.den, AddCommGroupWithOne.intCast_ofNat, Eq.mpr, Field.toDiv, Ring.toIntCast, Semiring.toNatCast, id, congrArg, Field.toRatCast, Field.ratCast_def, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, HPow.hPow, Nat, Nat.rawCast, Inv.inv, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf and 29 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

  11. problem Imo1975P6.imo1975_p6 line 104 source

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

    Statement uses: Polynomial, Real, Iff, Membership.mem, Set, Imo1975P6.solution_set, And, Exists, PNat, Eq, Polynomial.evalEval, HMul.hMul, HPow.hPow, Nat, HAdd.hAdd, OfNat.ofNat

    Proof uses: Iff.intro, HSub.hSub, RingHom, Polynomial.C, Polynomial.X, And.intro, Exists.intro, Subtype.mk, LT.lt, Eq.mpr, id, congr, congrArg, Eq.trans, Polynomial.eval, map_mul, Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_C, Polynomial.eval_ofNat and 129 more

    160 instances, coercions and auxiliary constants left out.

    Tactic trace: 68 steps

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