Compfiles/India1998P1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Indian Mathematical Olympiad 1998, problem 1

(a) Show that the product of two numbers of the form a² + 3b² is again of that form. (b) If an integer n is such that 7n is of the form a² + 3b², prove that n is also of that form.

Imports (4)
Imported by 1 file
  1. problem India1998P1.india1998_p1a line 28 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Int, Exists, Eq, HMul.hMul, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat

    Proof uses: Exists.intro, HSub.hSub, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.mpr, id, congrArg, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Mathlib.Tactic.Ring.Common.pow_add, Mathlib.Tactic.Ring.Common.single_pow, Mathlib.Tactic.Ring.Common.mul_pow_mul, Mathlib.Meta.NormNum.IsNat.to_raw_eq and 45 more

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  2. problem India1998P1.india1998_p1b line 32 source

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

    Statement uses: Int, Eq, HAdd.hAdd, HPow.hPow, Nat, OfNat.ofNat, HMul.hMul, Exists

    Proof uses: ZMod, Trans.trans, Eq.mpr, id, congrArg, Eq.trans, Int.cast_add, congr, Int.cast_pow, Int.cast_mul, Int.cast_ofNat, Eq.refl, MulZeroClass.zero_mul, Neg.neg, rfl, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.mp, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub and 91 more

    118 instances, coercions and auxiliary constants left out.

    Tactic trace: 68 steps

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