Compfiles/Usa1973P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 1973, Problem 4

Find all complex numbers x, y, z which satisfy x + y + z = x² + y² + z² = x³ + y³ + z³ = 3.

Imports (2)
Imported by 1 file
  1. determine Usa1973P4.solution_set line 26 source

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

    Statement uses: Set, Prod, Complex

    Proof uses: Singleton.singleton, Prod.mk, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

  2. problem Usa1973P4.usa1973_p4 line 28 source

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

    Statement uses: Complex, Iff, And, Eq, HAdd.hAdd, OfNat.ofNat, Nat, HPow.hPow, Membership.mem, Prod, Set, Usa1973P4.solution_set, Prod.mk

    Proof uses: Iff.intro, Prod.ext, Prod.snd

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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