Compfiles/Usa1977P3.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 1977, Problem 3

Prove that the product of the two real roots of x⁴ + x³ - 1 = 0 is a root of x⁶ + x⁴ + x³ - x² - 1 = 0.

Imports (6)
Imported by 1 file
  1. lemma Usa1977P3.sextic_of_zero_remainder Documented declaration: sextic_of_zero_remainder line 43 source

    Source documentation

    Suppose that x ^ 4 + x ^ 3 - 1 is divisible by the quadratic x ^ 2 - s * x + p, i.e. both coefficients of the remainder (s ^ 3 + s ^ 2 - 2 * p * s - p) * x + (p ^ 2 - p * (s ^ 2 + s) - 1) of the long division vanish. Then p is a root of the sextic x ^ 6 + x ^ 4 + x ^ 3 - x ^ 2 - 1.

    This is the Vieta elimination step of the problem: writing the four roots of the quartic as a, b, c, d with s = a + b and p = a * b, the two remainder relations are exactly the third and fourth elementary symmetric relations between the roots.

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

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

    Proof uses: Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.symm, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.refl, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.cast_pos and 112 more

    130 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

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

    lemma sextic_of_zero_remainder {s p : ℝ}
    (hr1 : s ^ 3 + s ^ 2 - 2 * p * s - p = 0)
    (hr0 : p ^ 2 - p * (s ^ 2 + s) - 1 = 0) :
    p ^ 6 + p ^ 4 + p ^ 3 - p ^ 2 - 1 = 0 := by
…
  2. problem Usa1977P3.usa1977_p3 line 72 source

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

    Statement uses: Real, Ne, Eq, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul

    Proof uses: rfl, Eq.mpr, id, congrArg, Mathlib.Tactic.Ring.of_eq, Int.rawCast, inferInstance, Ring, Int.negOfNat, Nat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow and 61 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 27 steps

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