Compfiles/Usa1988P2.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1988, Problem 2

The cubic x^3 + ax^2 + bx + c has real coefficients and three real roots r ≥ s ≥ t. Show that k = a^2 - 3b ≥ 0 and that √k ≤ r - t.

Imports (3)
Imported by 1 file
  1. lemma Usa1988P2.vieta Vieta's formulas for a and b, obtained by differentiating the polynomial identity once resp. twice and evaluating at 0 line 37 source

    Source comment

    Vieta's formulas for a and b, obtained by differentiating the polynomial identity once resp. twice and evaluating at 0.

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

    Statement uses: Real, Eq, Polynomial, HMul.hMul, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, And, Neg.neg

    Proof uses: And.intro, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat and 97 more

    133 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

    lemma vieta (a b c r s t : ℝ)
    (h : (X - C r) * (X - C s) * (X - C t) = X ^ 3 + C a * X ^ 2 + C b * X + C c) :
    a = -(r + s + t) ∧ b = r * s + s * t + t * r := by
…

    Mentions: h

  2. problem Usa1988P2.usa1988_p2 line 50 source

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

    Statement uses: Real, LE.le, Eq, Polynomial, HMul.hMul, HSub.hSub, Polynomial.X, RingHom, Polynomial.C, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, And, Real.sqrt

    Proof uses: Neg.neg, Usa1988P2.vieta, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.neg_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 68 more

    115 instances, coercions and auxiliary constants left out.

    Tactic trace: 15 steps

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