Compfiles/Usa2020P3.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

USA Mathematical Olympiad 2020 Problem 3

Let p be an odd prime. An integer x is called a quadratic non-residue if p does not divide x − t² for any integer t.

Denote by A the set of all integers a such that 1 ≤ a < p, and both a and 4 − a are quadratic non-residues. Calculate the remainder when the product of the elements of A is divided by p.

Imports (2)
Imported by 1 file
  1. determine Usamo2020P3.solution_val line 31 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: OfNat.ofNat

    1 instances, coercions and auxiliary constants left out.

  2. abbrev Usamo2020P3.setA' line 48 source
  3. abbrev Usamo2020P3.setB' line 51 source
  4. abbrev Usamo2020P3.setC' line 54 source
  5. lemma Usamo2020P3.isSquare_mul_iff_same line 57 source
  6. lemma Usamo2020P3.setC_eq_union line 65 source
  7. lemma Usamo2020P3.disjoint_AB line 75 source
  8. lemma Usamo2020P3.p_two_ne_zero line 79 source
  9. lemma Usamo2020P3.p_two_ne_four line 83 source
  10. lemma Usamo2020P3.two_mem_setC line 87 source
  11. lemma Usamo2020P3.map_mem_setB line 90 source
  12. lemma Usamo2020P3.fiber_prod line 99 source
  13. lemma Usamo2020P3.prod_C_erase_eq_prod_B line 124 source
  14. lemma Usamo2020P3.prod_B_ne_zero line 131 source
  15. problem Usamo2020P3.usa2020_p3 line 138 source

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

    Statement uses: Nat, Fact, Nat.Prime, Ne, OfNat.ofNat, Eq, ZMod, Finset.prod, Finset.filter, And, Not, IsSquare, HSub.hSub, Finset.univ, Usamo2020P3.solution_val

    Proof uses: mul_left_cancel₀, Trans.trans, HMul.hMul, Finset.erase, Eq.mpr, Union.union, Finset, id, congrArg, Finset.prod_union, mul_comm, Eq.refl, Eq.symm, Finset.mul_prod_erase, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Meta.NormNum.IsNat.to_eq, Mathlib.Meta.NormNum.isNat_natCast and 4 more

    98 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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