bump to nightly-2023-03-13-03

mathlib commit leanprover-community/mathlib@2af0836

Mathbin/NumberTheory/PellMatiyasevic.lean

@@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module number_theory.pell_matiyasevic
-! leanprover-community/mathlib commit a66d07e27d5b5b8ac1147cacfe353478e5c14002
+! leanprover-community/mathlib commit 2af0836443b4cfb5feda0df0051acdb398304931
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
+import Mathbin.Algebra.Star.Unitary
 import Mathbin.Data.Nat.Modeq
 import Mathbin.NumberTheory.Zsqrtd.Basic
 
@@ -196,19 +197,22 @@ theorem isPell_nat {x y : ℕ} : is_pell ⟨x, y⟩ ↔ x * x - d * y * y = 1 :=
       rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h] <;> rfl⟩
 #align pell.is_pell_nat Pell.isPell_nat
 
-theorem isPell_norm : ∀ {b : ℤ√d}, is_pell b ↔ b * b.conj = 1
+theorem isPell_norm : ∀ {b : ℤ√d}, is_pell b ↔ b * star b = 1
   | ⟨x, y⟩ => by simp [Zsqrtd.ext, is_pell, mul_comm] <;> ring_nf
 #align pell.is_pell_norm Pell.isPell_norm
 
+theorem isPell_iff_mem_unitary : ∀ {b : ℤ√d}, is_pell b ↔ b ∈ unitary (ℤ√d)
+  | ⟨x, y⟩ => by rw [unitary.mem_iff, is_pell_norm, mul_comm (star _), and_self_iff]
+#align pell.is_pell_iff_mem_unitary Pell.isPell_iff_mem_unitary
+
 theorem isPell_mul {b c : ℤ√d} (hb : is_pell b) (hc : is_pell c) : is_pell (b * c) :=
   is_pell_norm.2
-    (by
-      simp [mul_comm, mul_left_comm, Zsqrtd.conj_mul, Pell.isPell_norm.1 hb, Pell.isPell_norm.1 hc])
+    (by simp [mul_comm, mul_left_comm, star_mul, Pell.isPell_norm.1 hb, Pell.isPell_norm.1 hc])
 #align pell.is_pell_mul Pell.isPell_mul
 
-theorem isPell_conj : ∀ {b : ℤ√d}, is_pell b ↔ is_pell b.conj
-  | ⟨x, y⟩ => by simp [is_pell, Zsqrtd.conj]
-#align pell.is_pell_conj Pell.isPell_conj
+theorem isPell_star : ∀ {b : ℤ√d}, is_pell b ↔ is_pell (star b)
+  | ⟨x, y⟩ => by simp [is_pell, Zsqrtd.star_mk]
+#align pell.is_pell_star Pell.isPell_star
 
 @[simp]
 theorem pellZd_succ (n : ℕ) : pell_zd (n + 1) = pell_zd n * ⟨a, 1⟩ := by simp [Zsqrtd.ext]
@@ -286,7 +290,7 @@ theorem eq_pell_lem : ∀ (n) (b : ℤ√d), 1 ≤ b → is_pell b → b ≤ pel
     if ha : (⟨↑a, 1⟩ : ℤ√d) ≤ b then
       let ⟨m, e⟩ :=
         eq_pell_lem n (b * ⟨a, -1⟩) (by rw [← a1m] <;> exact mul_le_mul_of_nonneg_right ha am1p)
-          (is_pell_mul hp (is_pell_conj.1 is_pell_one))
+          (is_pell_mul hp (is_pell_star.1 is_pell_one))
           (by
             have t := mul_le_mul_of_nonneg_right h am1p <;>
               rwa [pell_zd_succ, mul_assoc, a1m, mul_one] at t)
@@ -365,7 +369,7 @@ theorem yn_add (m n) : yn (m + n) = xn m * yn n + yn m * xn n := by
     exact Int.ofNat.inj h
 #align pell.yn_add Pell.yn_add
 
-theorem pellZd_sub {m n} (h : n ≤ m) : pell_zd (m - n) = pell_zd m * (pell_zd n).conj :=
+theorem pellZd_sub {m n} (h : n ≤ m) : pell_zd (m - n) = pell_zd m * star (pell_zd n) :=
   by
   let t := pell_zd_add n (m - n)
   rw [add_tsub_cancel_of_le h] at t <;>

Mathbin/NumberTheory/Zsqrtd/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 
 ! This file was ported from Lean 3 source module number_theory.zsqrtd.basic
-! leanprover-community/mathlib commit a47cda9662ff3925c6df271090b5808adbca5b46
+! leanprover-community/mathlib commit 2af0836443b4cfb5feda0df0051acdb398304931
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -231,57 +231,28 @@ instance : Ring (ℤ√d) := by infer_instance
 instance : Distrib (ℤ√d) := by infer_instance
 
 /-- Conjugation in `ℤ√d`. The conjugate of `a + b √d` is `a - b √d`. -/
-def conj (z : ℤ√d) : ℤ√d :=
-  ⟨z.1, -z.2⟩
-#align zsqrtd.conj Zsqrtd.conj
+instance : Star (ℤ√d) where unit z := ⟨z.1, -z.2⟩
 
 @[simp]
-theorem conj_re (z : ℤ√d) : (conj z).re = z.re :=
+theorem star_mk (x y : ℤ) : star (⟨x, y⟩ : ℤ√d) = ⟨x, -y⟩ :=
   rfl
-#align zsqrtd.conj_re Zsqrtd.conj_re
+#align zsqrtd.star_mk Zsqrtd.star_mk
 
 @[simp]
-theorem conj_im (z : ℤ√d) : (conj z).im = -z.im :=
+theorem star_re (z : ℤ√d) : (star z).re = z.re :=
   rfl
-#align zsqrtd.conj_im Zsqrtd.conj_im
-
-/-- `conj` as an `add_monoid_hom`. -/
-def conjHom : ℤ√d →+ ℤ√d where
-  toFun := conj
-  map_add' := fun ⟨a, ai⟩ ⟨b, bi⟩ => ext.mpr ⟨rfl, neg_add _ _⟩
-  map_zero' := ext.mpr ⟨rfl, neg_zero⟩
-#align zsqrtd.conj_hom Zsqrtd.conjHom
-
-@[simp]
-theorem conj_zero : conj (0 : ℤ√d) = 0 :=
-  conj_hom.map_zero
-#align zsqrtd.conj_zero Zsqrtd.conj_zero
+#align zsqrtd.star_re Zsqrtd.star_re
 
 @[simp]
-theorem conj_one : conj (1 : ℤ√d) = 1 := by
-  simp only [Zsqrtd.ext, Zsqrtd.conj_re, Zsqrtd.conj_im, Zsqrtd.one_im, neg_zero, eq_self_iff_true,
-    and_self_iff]
-#align zsqrtd.conj_one Zsqrtd.conj_one
-
-@[simp]
-theorem conj_neg (x : ℤ√d) : (-x).conj = -x.conj :=
+theorem star_im (z : ℤ√d) : (star z).im = -z.im :=
   rfl
-#align zsqrtd.conj_neg Zsqrtd.conj_neg
-
-@[simp]
-theorem conj_add (x y : ℤ√d) : (x + y).conj = x.conj + y.conj :=
-  conj_hom.map_add x y
-#align zsqrtd.conj_add Zsqrtd.conj_add
+#align zsqrtd.star_im Zsqrtd.star_im
 
-@[simp]
-theorem conj_sub (x y : ℤ√d) : (x - y).conj = x.conj - y.conj :=
-  conj_hom.map_sub x y
-#align zsqrtd.conj_sub Zsqrtd.conj_sub
-
-@[simp]
-theorem conj_conj {d : ℤ} (x : ℤ√d) : x.conj.conj = x := by
-  simp only [ext, true_and_iff, conj_re, eq_self_iff_true, neg_neg, conj_im]
-#align zsqrtd.conj_conj Zsqrtd.conj_conj
+instance : StarRing (ℤ√d)
+    where
+  star_involutive x := ext.mpr ⟨rfl, neg_neg _⟩
+  star_mul a b := ext.mpr ⟨by simp <;> ring, by simp <;> ring⟩
+  star_add a b := ext.mpr ⟨rfl, neg_add _ _⟩
 
 instance : Nontrivial (ℤ√d) :=
   ⟨⟨0, 1, by decide⟩⟩
@@ -342,15 +313,9 @@ theorem smuld_val (n x y : ℤ) : sqrtd * (n : ℤ√d) * ⟨x, y⟩ = ⟨d * n
 theorem decompose {x y : ℤ} : (⟨x, y⟩ : ℤ√d) = x + sqrtd * y := by simp [ext]
 #align zsqrtd.decompose Zsqrtd.decompose
 
-theorem mul_conj {x y : ℤ} : (⟨x, y⟩ * conj ⟨x, y⟩ : ℤ√d) = x * x - d * y * y := by
+theorem mul_star {x y : ℤ} : (⟨x, y⟩ * star ⟨x, y⟩ : ℤ√d) = x * x - d * y * y := by
   simp [ext, sub_eq_add_neg, mul_comm]
-#align zsqrtd.mul_conj Zsqrtd.mul_conj
-
-theorem conj_mul {a b : ℤ√d} : conj (a * b) = conj a * conj b :=
-  by
-  simp [ext]
-  ring
-#align zsqrtd.conj_mul Zsqrtd.conj_mul
+#align zsqrtd.mul_star Zsqrtd.mul_star
 
 protected theorem coe_int_add (m n : ℤ) : (↑(m + n) : ℤ√d) = ↑m + ↑n :=
   (Int.castRingHom _).map_add _ _
@@ -571,18 +536,18 @@ def normMonoidHom : ℤ√d →* ℤ where
   map_one' := norm_one
 #align zsqrtd.norm_monoid_hom Zsqrtd.normMonoidHom
 
-theorem norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * n.conj := by
-  cases n <;> simp [norm, conj, Zsqrtd.ext, mul_comm, sub_eq_add_neg]
+theorem norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * star n := by
+  cases n <;> simp [norm, star, Zsqrtd.ext, mul_comm, sub_eq_add_neg]
 #align zsqrtd.norm_eq_mul_conj Zsqrtd.norm_eq_mul_conj
 
 @[simp]
 theorem norm_neg (x : ℤ√d) : (-x).norm = x.norm :=
-  coe_int_inj <| by simp only [norm_eq_mul_conj, conj_neg, neg_mul, mul_neg, neg_neg]
+  coe_int_inj <| by simp only [norm_eq_mul_conj, star_neg, neg_mul, mul_neg, neg_neg]
 #align zsqrtd.norm_neg Zsqrtd.norm_neg
 
 @[simp]
-theorem norm_conj (x : ℤ√d) : x.conj.norm = x.norm :=
-  coe_int_inj <| by simp only [norm_eq_mul_conj, conj_conj, mul_comm]
+theorem norm_conj (x : ℤ√d) : (star x).norm = x.norm :=
+  coe_int_inj <| by simp only [norm_eq_mul_conj, star_star, mul_comm]
 #align zsqrtd.norm_conj Zsqrtd.norm_conj
 
 theorem norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
@@ -597,12 +562,12 @@ theorem norm_eq_one_iff {x : ℤ√d} : x.norm.natAbs = 1 ↔ IsUnit x :=
       (le_total 0 (norm x)).casesOn
         (fun hx =>
           show x ∣ 1 from
-            ⟨x.conj, by
+            ⟨star x, by
               rwa [← Int.coe_nat_inj', Int.natAbs_of_nonneg hx, ← @Int.cast_inj (ℤ√d) _ _,
                 norm_eq_mul_conj, eq_comm] at h⟩)
         fun hx =>
         show x ∣ 1 from
-          ⟨-x.conj, by
+          ⟨-star x, by
             rwa [← Int.coe_nat_inj', Int.ofNat_natAbs_of_nonpos hx, ← @Int.cast_inj (ℤ√d) _ _,
               Int.cast_neg, norm_eq_mul_conj, neg_mul_eq_mul_neg, eq_comm] at h⟩,
     fun h => by

Mathbin/NumberTheory/Zsqrtd/GaussianInt.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module number_theory.zsqrtd.gaussian_int
-! leanprover-community/mathlib commit e1bccd6e40ae78370f01659715d3c948716e3b7e
+! leanprover-community/mathlib commit 2af0836443b4cfb5feda0df0051acdb398304931
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -44,6 +44,8 @@ and definitions about `zsqrtd` can easily be used.
 
 open Zsqrtd Complex
 
+open ComplexConjugate
+
 /-- The Gaussian integers, defined as `ℤ√(-1)`. -/
 @[reducible]
 def GaussianInt : Type :=
@@ -133,6 +135,13 @@ theorem to_complex_sub (x y : ℤ[i]) : ((x - y : ℤ[i]) : ℂ) = x - y :=
   toComplex.map_sub _ _
 #align gaussian_int.to_complex_sub GaussianInt.to_complex_sub
 
+@[simp]
+theorem to_complex_star (x : ℤ[i]) : ((star x : ℤ[i]) : ℂ) = conj (x : ℂ) :=
+  by
+  rw [to_complex_def₂, to_complex_def₂]
+  exact congr_arg₂ _ rfl (Int.cast_neg _)
+#align gaussian_int.to_complex_star GaussianInt.to_complex_star
+
 @[simp]
 theorem to_complex_inj {x y : ℤ[i]} : (x : ℂ) = y ↔ x = y := by
   cases x <;> cases y <;> simp [to_complex_def₂]
@@ -182,11 +191,11 @@ theorem natAbs_norm_eq (x : ℤ[i]) :
 instance : Div ℤ[i] :=
   ⟨fun x y =>
     let n := (norm y : ℚ)⁻¹
-    let c := y.conj
+    let c := star y
     ⟨round ((x * c).re * n : ℚ), round ((x * c).im * n : ℚ)⟩⟩
 
 theorem div_def (x y : ℤ[i]) :
-    x / y = ⟨round ((x * conj y).re / norm y : ℚ), round ((x * conj y).im / norm y : ℚ)⟩ :=
+    x / y = ⟨round ((x * star y).re / norm y : ℚ), round ((x * star y).im / norm y : ℚ)⟩ :=
   show Zsqrtd.mk _ _ = _ by simp [div_eq_mul_inv]
 #align gaussian_int.div_def GaussianInt.div_def
 

Mathbin/Topology/Order/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Yury Kudryashov
 
 ! This file was ported from Lean 3 source module topology.order.basic
-! leanprover-community/mathlib commit 0a0ec35061ed9960bf0e7ffb0335f44447b58977
+! leanprover-community/mathlib commit c985ae9840e06836a71db38de372f20acb49b790
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -3463,12 +3463,16 @@ theorem frontier_Iio [NoMinOrder α] {a : α} : frontier (Iio a) = {a} :=
 #align frontier_Iio frontier_Iio
 -/
 
-#print frontier_Icc /-
+/- warning: frontier_Icc -> frontier_Icc is a dubious translation:
+lean 3 declaration is
+  forall {α : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} α] [_inst_2 : LinearOrder.{u1} α] [_inst_3 : OrderTopology.{u1} α _inst_1 (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2))))] [_inst_4 : DenselyOrdered.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2)))))] [_inst_5 : NoMinOrder.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2)))))] [_inst_6 : NoMaxOrder.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2)))))] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2))))) a b) -> (Eq.{succ u1} (Set.{u1} α) (frontier.{u1} α _inst_1 (Set.Icc.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_2)))) a b)) (Insert.insert.{u1, u1} α (Set.{u1} α) (Set.hasInsert.{u1} α) a (Singleton.singleton.{u1, u1} α (Set.{u1} α) (Set.hasSingleton.{u1} α) b)))
+but is expected to have type
+  forall {α : Type.{u1}} [_inst_1 : TopologicalSpace.{u1} α] [_inst_2 : LinearOrder.{u1} α] [_inst_3 : OrderTopology.{u1} α _inst_1 (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2)))))] [_inst_4 : DenselyOrdered.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2))))))] [_inst_5 : NoMinOrder.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2))))))] [_inst_6 : NoMaxOrder.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2))))))] {a : α} {b : α}, (LT.lt.{u1} α (Preorder.toLT.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2)))))) a b) -> (Eq.{succ u1} (Set.{u1} α) (frontier.{u1} α _inst_1 (Set.Icc.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_2))))) a b)) (Insert.insert.{u1, u1} α (Set.{u1} α) (Set.instInsertSet.{u1} α) a (Singleton.singleton.{u1, u1} α (Set.{u1} α) (Set.instSingletonSet.{u1} α) b)))
+Case conversion may be inaccurate. Consider using '#align frontier_Icc frontier_Iccₓ'. -/
 @[simp]
-theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a < b) :
-    frontier (Icc a b) = {a, b} := by simp [frontier, le_of_lt h, Icc_diff_Ioo_same]
+theorem frontier_Icc [NoMinOrder α] [NoMaxOrder α] {a b : α} (h : a ≤ b) :
+    frontier (Icc a b) = {a, b} := by simp [frontier, h, Icc_diff_Ioo_same]
 #align frontier_Icc frontier_Icc
--/
 
 #print frontier_Ioo /-
 @[simp]

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`f24cc2891c0e328f0ee8c57387103aa462c44b5e`](https://github.com/leanprover-community/mathlib/commit/f24cc2891c0e328f0ee8c57387103aa462c44b5e)
+Tracking mathlib commit: [`2af0836443b4cfb5feda0df0051acdb398304931`](https://github.com/leanprover-community/mathlib/commit/2af0836443b4cfb5feda0df0051acdb398304931)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -4,9 +4,9 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "eaacdde649479705c1249776c305e0c5e246c123",
+    "rev": "511c1c673344145e462ebae2e0eb4104ead6c2e1",
     "name": "lean3port",
-    "inputRev?": "eaacdde649479705c1249776c305e0c5e246c123"}},
+    "inputRev?": "511c1c673344145e462ebae2e0eb4104ead6c2e1"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "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-03-13-00"
+def tag : String := "nightly-2023-03-13-03"
 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"@"eaacdde649479705c1249776c305e0c5e246c123"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"511c1c673344145e462ebae2e0eb4104ead6c2e1"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-f24cc2891c0e328f0ee8c57387103aa462c44b5e
+2af0836443b4cfb5feda0df0051acdb398304931