Compfiles/Imo1963P4.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1963, Problem 4

Find all solutions x₁,x₂,x₃,x₄,x₅ of the system

x₅ + x₂ = yx₁ x₁ + x₃ = yx₂ x₂ + x₄ = yx₃ x₃ + x₅ = yx₄ x₄ + x₁ = yx₅

where y is a parameter.

Imports (2)
Imported by 1 file
  1. determine Imo1963P4.SolutionSet line 33 source

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

    Statement uses: Real, Set, Prod

    Proof uses: Set.ofPred, Imo1963P4.SolutionSet.match_1, Or, And, Eq, OfNat.ofNat, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, Exists, HMul.hMul, Neg.neg

    19 instances, coercions and auxiliary constants left out.

  2. problem Imo1963P4.imo1963_p4 line 44 source

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

    Statement uses: Real, Iff, Membership.mem, Prod, Set, Imo1963P4.SolutionSet, Prod.mk, And, Eq, HAdd.hAdd, HMul.hMul

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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