Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1977P3

module

public import Mathlib.Analysis.Normed.Field.Basic
public import Mathlib.Tactic.FieldSimp
public import Mathlib.Tactic.LinearCombination
public import Mathlib.Tactic.NormNum
public import Mathlib.Tactic.Ring

public section


/-!
# 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.
-/

namespace Usa1977P3

theorem usa1977_p3 (a b : ℝ) (hab : a ≠ b)
    (ha : a ^ 4 + a ^ 3 - 1 = 0) (hb : b ^ 4 + b ^ 3 - 1 = 0) :
    (a * b) ^ 6 + (a * b) ^ 4 + (a * b) ^ 3 - (a * b) ^ 2 - 1 = 0 := sorry

end Usa1977P3

File author(s): Kimi K3

This problem has a complete formalized solution.