Compfiles/Imo1973P3.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1973, Problem 3

Let $a$ and $b$ be real numbers for which the equation $x^4 + ax^3 + bx^2 + ax + 1 = 0$ has at least one real solution. For all such pairs $(a, b)$, find the minimum value of $a^2 + b^2$.

Imports (2)
Imported by 1 file
  1. abbrev Imo1973P3.solution line 31 source

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

    Statement uses: Real

    Proof uses: HDiv.hDiv, OfNat.ofNat

    7 instances, coercions and auxiliary constants left out.

  2. lemma Imo1973P3.aux_1 line 35 source

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

    Statement uses: Real, Exists, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, LE.le, HDiv.hDiv

    Proof uses: Eq.refl, Ne, id, False.elim, False, Eq.mp, Eq.trans, congrFun', congrArg, congr, zero_pow, of_eq_true, Not, True, not_false_eq_true, MulZeroClass.mul_zero, add_zero, zero_add, HSub.hSub, Eq.mpr and 182 more

    223 instances, coercions and auxiliary constants left out.

    Tactic trace: 117 steps

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

  3. problem Imo1973P3.imo1973_p3 line 139 source

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

    Statement uses: Set, Prod, Real, Eq, Set.ofPred, Imo1973P3.imo1973_p3.match_1, Exists, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, IsLeast, And, Membership.mem, Prod.fst, Prod.snd, Imo1973P3.solution

    Proof uses: And.intro, lowerBounds, Eq.mpr, Prod.mk, id, congrFun', congrArg, funext, Exists.intro, HDiv.hDiv, Neg.neg, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Meta.NormNum.IsInt.to_isNat, Mathlib.Meta.NormNum.isInt_add, Int.negOfNat, Int.ofNat, Eq.refl, Mathlib.Meta.NormNum.IsRat.to_isInt, Mathlib.Meta.NormNum.isRat_add and 39 more

    78 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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