bump to nightly-2023-06-26-15

mathlib commit leanprover-community/mathlib@fdc286c

Mathbin/NumberTheory/LegendreSymbol/QuadraticChar/GaussSum.lean

@@ -34,13 +34,16 @@ open ZMod MulChar
 
 variable {F : Type _} [Field F] [Fintype F]
 
+#print quadraticChar_two /-
 /-- The value of the quadratic character at `2` -/
 theorem quadraticChar_two [DecidableEq F] (hF : ringChar F ≠ 2) :
     quadraticChar F 2 = χ₈ (Fintype.card F) :=
   IsQuadratic.eq_of_eq_coe (quadraticChar_isQuadratic F) isQuadratic_χ₈ hF
     ((quadraticChar_eq_pow_of_char_ne_two' hF 2).trans (FiniteField.two_pow_card hF))
 #align quadratic_char_two quadraticChar_two
+-/
 
+#print FiniteField.isSquare_two_iff /-
 /-- `2` is a square in `F` iff `#F` is not congruent to `3` or `5` mod `8`. -/
 theorem FiniteField.isSquare_two_iff :
     IsSquare (2 : F) ↔ Fintype.card F % 8 ≠ 3 ∧ Fintype.card F % 8 ≠ 5 := by
@@ -63,14 +66,18 @@ theorem FiniteField.isSquare_two_iff :
     generalize Fintype.card F % 8 = n
     decide!
 #align finite_field.is_square_two_iff FiniteField.isSquare_two_iff
+-/
 
+#print quadraticChar_neg_two /-
 /-- The value of the quadratic character at `-2` -/
 theorem quadraticChar_neg_two [DecidableEq F] (hF : ringChar F ≠ 2) :
     quadraticChar F (-2) = χ₈' (Fintype.card F) := by
   rw [(by norm_num : (-2 : F) = -1 * 2), map_mul, χ₈'_eq_χ₄_mul_χ₈, quadraticChar_neg_one hF,
     quadraticChar_two hF, @cast_nat_cast _ (ZMod 4) _ _ _ (by norm_num : 4 ∣ 8)]
 #align quadratic_char_neg_two quadraticChar_neg_two
+-/
 
+#print FiniteField.isSquare_neg_two_iff /-
 /-- `-2` is a square in `F` iff `#F` is not congruent to `5` or `7` mod `8`. -/
 theorem FiniteField.isSquare_neg_two_iff :
     IsSquare (-2 : F) ↔ Fintype.card F % 8 ≠ 5 ∧ Fintype.card F % 8 ≠ 7 := by
@@ -93,7 +100,9 @@ theorem FiniteField.isSquare_neg_two_iff :
     generalize Fintype.card F % 8 = n
     decide!
 #align finite_field.is_square_neg_two_iff FiniteField.isSquare_neg_two_iff
+-/
 
+#print quadraticChar_card_card /-
 /-- The relation between the values of the quadratic character of one field `F` at the
 cardinality of another field `F'` and of the quadratic character of `F'` at the cardinality
 of `F`. -/
@@ -119,7 +128,9 @@ theorem quadraticChar_card_card [DecidableEq F] (hF : ringChar F ≠ 2) {F' : Ty
     (is_quadratic.eq_of_eq_coe (quadraticChar_isQuadratic F') (quadraticChar_isQuadratic F) hF'
         h).symm
 #align quadratic_char_card_card quadraticChar_card_card
+-/
 
+#print quadraticChar_odd_prime /-
 /-- The value of the quadratic character at an odd prime `p` different from `ring_char F`. -/
 theorem quadraticChar_odd_prime [DecidableEq F] (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime]
     (hp₁ : p ≠ 2) (hp₂ : ringChar F ≠ p) :
@@ -131,7 +142,9 @@ theorem quadraticChar_odd_prime [DecidableEq F] (hF : ringChar F ≠ 2) {p : ℕ
       (ne_of_eq_of_ne (ring_char_zmod_n p) hp₂.symm)
   rwa [card p] at h 
 #align quadratic_char_odd_prime quadraticChar_odd_prime
+-/
 
+#print FiniteField.isSquare_odd_prime_iff /-
 /-- An odd prime `p` is a square in `F` iff the quadratic character of `zmod p` does not
 take the value `-1` on `χ₄(#F) * #F`. -/
 theorem FiniteField.isSquare_odd_prime_iff (hF : ringChar F ≠ 2) {p : ℕ} [Fact p.Prime]
@@ -154,6 +167,7 @@ theorem FiniteField.isSquare_odd_prime_iff (hF : ringChar F ≠ 2) {p : ℕ} [Fa
       quadraticChar_odd_prime hF hp]
     exact hFp
 #align finite_field.is_square_odd_prime_iff FiniteField.isSquare_odd_prime_iff
+-/
 
 end SpecialValues
 

Mathbin/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean

@@ -60,24 +60,29 @@ namespace legendreSym
 
 variable (hp : p ≠ 2)
 
+#print legendreSym.at_two /-
 /-- `legendre_sym p 2` is given by `χ₈ p`. -/
 theorem at_two : legendreSym p 2 = χ₈ p := by
   simp only [legendreSym, card p, quadraticChar_two ((ring_char_zmod_n p).substr hp), Int.cast_bit0,
     Int.cast_one]
 #align legendre_sym.at_two legendreSym.at_two
+-/
 
+#print legendreSym.at_neg_two /-
 /-- `legendre_sym p (-2)` is given by `χ₈' p`. -/
 theorem at_neg_two : legendreSym p (-2) = χ₈' p := by
   simp only [legendreSym, card p, quadraticChar_neg_two ((ring_char_zmod_n p).substr hp),
     Int.cast_bit0, Int.cast_one, Int.cast_neg]
 #align legendre_sym.at_neg_two legendreSym.at_neg_two
+-/
 
 end legendreSym
 
 namespace ZMod
 
 variable (hp : p ≠ 2)
 
+#print ZMod.exists_sq_eq_two_iff /-
 /-- `2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `7` mod `8`. -/
 theorem exists_sq_eq_two_iff : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7 :=
   by
@@ -89,7 +94,9 @@ theorem exists_sq_eq_two_iff : IsSquare (2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 7
   generalize hm : p % 8 = m; clear! p
   decide!
 #align zmod.exists_sq_eq_two_iff ZMod.exists_sq_eq_two_iff
+-/
 
+#print ZMod.exists_sq_eq_neg_two_iff /-
 /-- `-2` is a square modulo an odd prime `p` iff `p` is congruent to `1` or `3` mod `8`. -/
 theorem exists_sq_eq_neg_two_iff : IsSquare (-2 : ZMod p) ↔ p % 8 = 1 ∨ p % 8 = 3 :=
   by
@@ -101,6 +108,7 @@ theorem exists_sq_eq_neg_two_iff : IsSquare (-2 : ZMod p) ↔ p % 8 = 1 ∨ p %
   generalize hm : p % 8 = m; clear! p
   decide!
 #align zmod.exists_sq_eq_neg_two_iff ZMod.exists_sq_eq_neg_two_iff
+-/
 
 end ZMod
 
@@ -122,6 +130,7 @@ namespace legendreSym
 
 open ZMod
 
+#print legendreSym.quadratic_reciprocity /-
 /-- The Law of Quadratic Reciprocity: if `p` and `q` are distinct odd primes, then
 `(q / p) * (p / q) = (-1)^((p-1)(q-1)/4)`. -/
 theorem quadratic_reciprocity (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
@@ -139,7 +148,9 @@ theorem quadratic_reciprocity (hp : p ≠ 2) (hq : q ≠ 2) (hpq : p ≠ q) :
     quadraticChar_sq_one (prime_ne_zero q p hpq.symm), mul_one, pow_mul, χ₄_eq_neg_one_pow hp₁, nc',
     map_pow, quadraticChar_neg_one hq₂, card q, χ₄_eq_neg_one_pow hq₁]
 #align legendre_sym.quadratic_reciprocity legendreSym.quadratic_reciprocity
+-/
 
+#print legendreSym.quadratic_reciprocity' /-
 /-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes, then
 `(q / p) = (-1)^((p-1)(q-1)/4) * (p / q)`. -/
 theorem quadratic_reciprocity' (hp : p ≠ 2) (hq : q ≠ 2) :
@@ -152,15 +163,19 @@ theorem quadratic_reciprocity' (hp : p ≠ 2) (hq : q ≠ 2) :
     have : ((q : ℤ) : ZMod p) ≠ 0 := by exact_mod_cast prime_ne_zero p q h
     simpa only [mul_assoc, ← pow_two, sq_one p this, mul_one] using qr
 #align legendre_sym.quadratic_reciprocity' legendreSym.quadratic_reciprocity'
+-/
 
+#print legendreSym.quadratic_reciprocity_one_mod_four /-
 /-- The Law of Quadratic Reciprocity: if `p` and `q` are odd primes and `p % 4 = 1`,
 then `(q / p) = (p / q)`. -/
 theorem quadratic_reciprocity_one_mod_four (hp : p % 4 = 1) (hq : q ≠ 2) :
     legendreSym q p = legendreSym p q := by
   rw [quadratic_reciprocity' (prime.mod_two_eq_one_iff_ne_two.mp (odd_of_mod_four_eq_one hp)) hq,
     pow_mul, neg_one_pow_div_two_of_one_mod_four hp, one_pow, one_mul]
 #align legendre_sym.quadratic_reciprocity_one_mod_four legendreSym.quadratic_reciprocity_one_mod_four
+-/
 
+#print legendreSym.quadratic_reciprocity_three_mod_four /-
 /-- The Law of Quadratic Reciprocity: if `p` and `q` are primes that are both congruent
 to `3` mod `4`, then `(q / p) = -(p / q)`. -/
 theorem quadratic_reciprocity_three_mod_four (hp : p % 4 = 3) (hq : q % 4 = 3) :
@@ -170,13 +185,15 @@ theorem quadratic_reciprocity_three_mod_four (hp : p % 4 = 3) (hq : q % 4 = 3) :
   rw [quadratic_reciprocity', pow_mul, nop hp, nop hq, neg_one_mul] <;>
     rwa [← prime.mod_two_eq_one_iff_ne_two, odd_of_mod_four_eq_three]
 #align legendre_sym.quadratic_reciprocity_three_mod_four legendreSym.quadratic_reciprocity_three_mod_four
+-/
 
 end legendreSym
 
 namespace ZMod
 
 open legendreSym
 
+#print ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one /-
 /-- If `p` and `q` are odd primes and `p % 4 = 1`, then `q` is a square mod `p` iff
 `p` is a square mod `q`. -/
 theorem exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠ 2) :
@@ -188,14 +205,17 @@ theorem exists_sq_eq_prime_iff_of_mod_four_eq_one (hp1 : p % 4 = 1) (hq1 : q ≠
     rw [← eq_one_iff' p (prime_ne_zero p q h), ← eq_one_iff' q (prime_ne_zero q p h.symm),
       quadratic_reciprocity_one_mod_four hp1 hq1]
 #align zmod.exists_sq_eq_prime_iff_of_mod_four_eq_one ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one
+-/
 
+#print ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three /-
 /-- If `p` and `q` are distinct primes that are both congruent to `3` mod `4`, then `q` is
 a square mod `p` iff `p` is a nonsquare mod `q`. -/
 theorem exists_sq_eq_prime_iff_of_mod_four_eq_three (hp3 : p % 4 = 3) (hq3 : q % 4 = 3)
     (hpq : p ≠ q) : IsSquare (q : ZMod p) ↔ ¬IsSquare (p : ZMod q) := by
   rw [← eq_one_iff' p (prime_ne_zero p q hpq), ← eq_neg_one_iff' q,
     quadratic_reciprocity_three_mod_four hp3 hq3, neg_inj]
 #align zmod.exists_sq_eq_prime_iff_of_mod_four_eq_three ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three
+-/
 
 end ZMod
 

Mathbin/NumberTheory/Wilson.lean

@@ -116,5 +116,5 @@ theorem prime_iff_fac_equiv_neg_one (h : n ≠ 1) : Prime n ↔ ((n - 1)! : ZMod
 
 end Nat
 
-assert_not_exists legendre_sym.quadratic_reciprocity
+assert_not_exists legendreSym.quadratic_reciprocity
 

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "3b322644acf968b954d1d2be2e632ea5ff600260",
+    "rev": "692cdf8cee9634898a3714476d82761cbd42b08f",
     "name": "lean3port",
-    "inputRev?": "3b322644acf968b954d1d2be2e632ea5ff600260"}},
+    "inputRev?": "692cdf8cee9634898a3714476d82761cbd42b08f"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "5775c8521eb0918aff275c9e598ad2c2f187f5de",
+    "rev": "dc08a85ff7e500319a05e0a4140a42bc4864b869",
     "name": "mathlib",
-    "inputRev?": "5775c8521eb0918aff275c9e598ad2c2f187f5de"}},
+    "inputRev?": "dc08a85ff7e500319a05e0a4140a42bc4864b869"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-26-13"
+def tag : String := "nightly-2023-06-26-15"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"3b322644acf968b954d1d2be2e632ea5ff600260"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"692cdf8cee9634898a3714476d82761cbd42b08f"
 
 @[default_target]
 lean_lib Mathbin where