Compfiles/Usa1984P1.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

3 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1984, Problem 1

Two roots of the real quartic x⁴ - 18x³ + ax² + 200x - 1984 = 0 have product -32. Find a.

Imports (6)
Imported by 1 file
  1. determine Usa1984P1.solution line 31 source

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

    Statement uses: Real

    Proof uses: OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. theorem Usa1984P1.eq_X_sq_add_of_monic_of_natDegree_eq_two A monic quadratic polynomial is determined by its lower coefficients line 36 source

    Source documentation

    A monic quadratic polynomial is determined by its lower coefficients.

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

    Statement uses: CommRing, Polynomial, Polynomial.Monic, Eq, Nat, Polynomial.natDegree, OfNat.ofNat, HAdd.hAdd, HPow.hPow, Polynomial.X, HMul.hMul, RingHom, Polynomial.C, Finsupp, Polynomial.coeff

    Proof uses: Eq.mpr, Finset.sum, Finset.range, id, Eq.rec, Eq.refl, Eq.trans, congrArg, Polynomial.as_sum_range_C_mul_X_pow, Finset.sum_range_succ, Finset.sum_range_zero, Polynomial.Monic.coeff_natDegree, Eq.mp, congrFun', map_one, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.cast_zero, Mathlib.Meta.NormNum.isNat_ofNat and 28 more

    66 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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

    theorem eq_X_sq_add_of_monic_of_natDegree_eq_two {R : Type*} [CommRing R] {q : R[X]}
    (hm : q.Monic) (hd : q.natDegree = 2) :
    q = X ^ 2 + C (q.coeff 1) * X + C (q.coeff 0) := by
…
  3. problem Usa1984P1.usa1984_p1 line 50 source

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

    Statement uses: Real, Polynomial, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat, HMul.hMul, RingHom, Polynomial.C, Complex, Ne, AlgHom, Polynomial.aeval, Neg.neg, Usa1984P1.solution

    Proof uses: Polynomial.map, Algebra.algebraMap, rfl, Eq.mpr, id, congrArg, of_eq_true, Eq.trans, True, congr, congrFun', sub_eq_add_neg, Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_neg, Polynomial.map_mul, Polynomial.map_C, map_neg, neg_mul and 154 more

    211 instances, coercions and auxiliary constants left out.

    Tactic trace: 77 steps

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