Compfiles/Imo1961P3.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1961, Problem 3

Solve the equation

cosⁿ x - sinⁿ x = 1,

where n is a given positive integer.

Imports (3)
Imported by 1 file
  1. determine Imo1961P3.solutionSet line 35 source

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

    Statement uses: PNat, Set, Real

    Proof uses: Set.ofPred, Or, And, Exists, Int, Eq, HMul.hMul, Real.pi, Even, Nat, OfNat.ofNat, Odd, HAdd.hAdd, Neg.neg, HDiv.hDiv

    16 instances, coercions and auxiliary constants left out.

  2. problem Imo1961P3.imo1961_p3 line 39 source

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

    Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Iff, Membership.mem, Set, Imo1961P3.solutionSet, Subtype.mk, Eq, HSub.hSub, HPow.hPow, Real.cos, Real.sin

    Proof uses: Ne, Nat.ne_zero_of_lt, Iff.intro, And, Exists, Int, HMul.hMul, Real.pi, Even, Or, Odd, HAdd.hAdd, Neg.neg, HDiv.hDiv, Eq.mpr, id, congrArg, Real.sin_int_mul_pi, zero_pow, sub_zero and 115 more

    198 instances, coercions and auxiliary constants left out.

    Tactic trace: 59 steps

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