Compfiles/Imo1965P2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1965, Problem 2

Suppose that a₁₁x₁ + a₁₂x₂ + a₁₃x₃ = 0 a₂₁x₁ + a₂₂x₂ + a₂₃x₃ = 0 a₃₁x₁ + a₃₂x₂ + a₃₃x₃ = 0

where (A) a₁₁, a₂₂, a₃₃ are positive (B) the remaining aᵢⱼ are negative (C) in each row i, the sum of the coefficients aᵢⱼ is positive.

Prove that x₁ = x₂ = x₃ = 0.

Imports (2)
Imported by 1 file
  1. abbrev Imo1965P2.propEqs line 37 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real

    Proof uses: Eq, Finset.sum, Finset.univ, HMul.hMul

    8 instances, coercions and auxiliary constants left out.

  2. lemma Imo1965P2.lemma0 line 40 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Function.Bijective, Imo1965P2.propEqs, Function.comp

    Proof uses: id, Eq, Finset.sum, Finset.univ, HMul.hMul, Eq.mpr, congrArg, Function.Bijective.sum_comp

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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

  3. abbrev Imo1965P2.propsAB line 48 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real

    Proof uses: ite, Eq, LT.lt

    6 instances, coercions and auxiliary constants left out.

  4. lemma Imo1965P2.lemma1 line 51 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Function.Bijective, Imo1965P2.propsAB

    Proof uses: ite, Eq, LT.lt, dite, Eq.mpr, id, ite_eq_left, Eq.mp, Eq.trans, True, ite_congr, eq_self, Eq.refl, Not, ite_eq_left_of_eq_true, ite_eq_right, Ne, And.left, Function.Injective, Function.Surjective and 2 more

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

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

  5. lemma Imo1965P2.lemma2 line 65 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Function.Bijective, LT.lt, Finset.sum, Finset.univ

    Proof uses: Eq.mpr, id, Eq, congrArg, Function.Bijective.sum_comp

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  6. problem Imo1965P2.imo1965_p2 line 76 source

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

    Statement uses: Fin, OfNat.ofNat, Nat, Real, Eq, Finset.sum, Finset.univ, HMul.hMul, ite, LT.lt

    Proof uses: LE.le, abs, Not, Or, Classical.em, HAdd.hAdd, Eq.mpr, id, congrArg, Fin.sum_univ_three, add_rotate, Eq.refl, Eq.symm, Neg.neg, lt_of_not_ge, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr and 118 more

    125 instances, coercions and auxiliary constants left out.

    Tactic trace: 62 steps

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