bump to nightly-2024-02-18-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/CategoryTheory/Monoidal/Opposite.lean

@@ -53,28 +53,28 @@ def unmop (X : Cᴹᵒᵖ) : C :=
 #align category_theory.monoidal_opposite.unmop CategoryTheory.MonoidalOpposite.unmop
 -/
 
-#print CategoryTheory.MonoidalOpposite.op_injective /-
-theorem op_injective : Function.Injective (mop : C → Cᴹᵒᵖ) := fun _ _ => id
-#align category_theory.monoidal_opposite.op_injective CategoryTheory.MonoidalOpposite.op_injective
+#print CategoryTheory.MonoidalOpposite.mop_injective /-
+theorem mop_injective : Function.Injective (mop : C → Cᴹᵒᵖ) := fun _ _ => id
+#align category_theory.monoidal_opposite.op_injective CategoryTheory.MonoidalOpposite.mop_injective
 -/
 
-#print CategoryTheory.MonoidalOpposite.unop_injective /-
-theorem unop_injective : Function.Injective (unmop : Cᴹᵒᵖ → C) := fun _ _ => id
-#align category_theory.monoidal_opposite.unop_injective CategoryTheory.MonoidalOpposite.unop_injective
+#print CategoryTheory.MonoidalOpposite.unmop_injective /-
+theorem unmop_injective : Function.Injective (unmop : Cᴹᵒᵖ → C) := fun _ _ => id
+#align category_theory.monoidal_opposite.unop_injective CategoryTheory.MonoidalOpposite.unmop_injective
 -/
 
-#print CategoryTheory.MonoidalOpposite.op_inj_iff /-
+#print CategoryTheory.MonoidalOpposite.mop_inj_iff /-
 @[simp]
-theorem op_inj_iff (x y : C) : mop x = mop y ↔ x = y :=
+theorem mop_inj_iff (x y : C) : mop x = mop y ↔ x = y :=
   Iff.rfl
-#align category_theory.monoidal_opposite.op_inj_iff CategoryTheory.MonoidalOpposite.op_inj_iff
+#align category_theory.monoidal_opposite.op_inj_iff CategoryTheory.MonoidalOpposite.mop_inj_iff
 -/
 
-#print CategoryTheory.MonoidalOpposite.unop_inj_iff /-
+#print CategoryTheory.MonoidalOpposite.unmop_inj_iff /-
 @[simp]
-theorem unop_inj_iff (x y : Cᴹᵒᵖ) : unmop x = unmop y ↔ x = y :=
+theorem unmop_inj_iff (x y : Cᴹᵒᵖ) : unmop x = unmop y ↔ x = y :=
   Iff.rfl
-#align category_theory.monoidal_opposite.unop_inj_iff CategoryTheory.MonoidalOpposite.unop_inj_iff
+#align category_theory.monoidal_opposite.unop_inj_iff CategoryTheory.MonoidalOpposite.unmop_inj_iff
 -/
 
 #print CategoryTheory.MonoidalOpposite.mop_unmop /-
@@ -126,31 +126,32 @@ def Quiver.Hom.unmop {X Y : Cᴹᵒᵖ} (f : X ⟶ Y) : unmop X ⟶ unmop Y :=
 
 namespace CategoryTheory
 
-#print CategoryTheory.mop_inj /-
-theorem mop_inj {X Y : C} : Function.Injective (Quiver.Hom.mop : (X ⟶ Y) → (mop X ⟶ mop Y)) :=
-  fun _ _ H => congr_arg Quiver.Hom.unmop H
-#align category_theory.mop_inj CategoryTheory.mop_inj
+#print Quiver.Hom.mop_inj /-
+theorem Quiver.Hom.mop_inj {X Y : C} :
+    Function.Injective (Quiver.Hom.mop : (X ⟶ Y) → (mop X ⟶ mop Y)) := fun _ _ H =>
+  congr_arg Quiver.Hom.unmop H
+#align category_theory.mop_inj Quiver.Hom.mop_inj
 -/
 
-#print CategoryTheory.unmop_inj /-
-theorem unmop_inj {X Y : Cᴹᵒᵖ} :
+#print Quiver.Hom.unmop_inj /-
+theorem Quiver.Hom.unmop_inj {X Y : Cᴹᵒᵖ} :
     Function.Injective (Quiver.Hom.unmop : (X ⟶ Y) → (unmop X ⟶ unmop Y)) := fun _ _ H =>
   congr_arg Quiver.Hom.mop H
-#align category_theory.unmop_inj CategoryTheory.unmop_inj
+#align category_theory.unmop_inj Quiver.Hom.unmop_inj
 -/
 
-#print CategoryTheory.unmop_mop /-
+#print Quiver.Hom.unmop_mop /-
 @[simp]
-theorem unmop_mop {X Y : C} {f : X ⟶ Y} : f.mop.unmop = f :=
+theorem Quiver.Hom.unmop_mop {X Y : C} {f : X ⟶ Y} : f.mop.unmop = f :=
   rfl
-#align category_theory.unmop_mop CategoryTheory.unmop_mop
+#align category_theory.unmop_mop Quiver.Hom.unmop_mop
 -/
 
-#print CategoryTheory.mop_unmop /-
+#print Quiver.Hom.mop_unmop /-
 @[simp]
-theorem mop_unmop {X Y : Cᴹᵒᵖ} {f : X ⟶ Y} : f.unmop.mop = f :=
+theorem Quiver.Hom.mop_unmop {X Y : Cᴹᵒᵖ} {f : X ⟶ Y} : f.unmop.mop = f :=
   rfl
-#align category_theory.mop_unmop CategoryTheory.mop_unmop
+#align category_theory.mop_unmop Quiver.Hom.mop_unmop
 -/
 
 #print CategoryTheory.mop_comp /-
@@ -205,8 +206,8 @@ variable {X Y : C}
 def mop (f : X ≅ Y) : mop X ≅ mop Y where
   Hom := f.Hom.mop
   inv := f.inv.mop
-  hom_inv_id' := unmop_inj f.hom_inv_id
-  inv_hom_id' := unmop_inj f.inv_hom_id
+  hom_inv_id' := Quiver.Hom.unmop_inj f.hom_inv_id
+  inv_hom_id' := Quiver.Hom.unmop_inj f.inv_hom_id
 #align category_theory.iso.mop CategoryTheory.Iso.mop
 -/
 

Mathbin/GroupTheory/Exponent.lean

@@ -79,17 +79,17 @@ noncomputable def exponent :=
 
 variable {G}
 
-#print Monoid.exponentExists_iff_ne_zero /-
+#print Monoid.exponent_ne_zero /-
 @[to_additive]
-theorem exponentExists_iff_ne_zero : ExponentExists G ↔ exponent G ≠ 0 :=
+theorem exponent_ne_zero : ExponentExists G ↔ exponent G ≠ 0 :=
   by
   rw [exponent]
   split_ifs
   · simp [h, @not_lt_zero' ℕ]
   --if this isn't done this way, `to_additive` freaks
   · tauto
-#align monoid.exponent_exists_iff_ne_zero Monoid.exponentExists_iff_ne_zero
-#align add_monoid.exponent_exists_iff_ne_zero AddMonoid.exponentExists_iff_ne_zero
+#align monoid.exponent_exists_iff_ne_zero Monoid.exponent_ne_zero
+#align add_monoid.exponent_exists_iff_ne_zero AddMonoid.exponent_ne_zero
 -/
 
 #print Monoid.exponent_eq_zero_iff /-
@@ -293,16 +293,16 @@ theorem exponent_eq_zero_iff_range_orderOf_infinite (h : ∀ g : G, 0 < orderOf
 #align add_monoid.exponent_eq_zero_iff_range_order_of_infinite AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite
 -/
 
-#print Monoid.lcm_order_eq_exponent /-
+#print Monoid.lcm_orderOf_eq_exponent /-
 @[to_additive lcm_add_order_eq_exponent]
-theorem lcm_order_eq_exponent [Fintype G] : (Finset.univ : Finset G).lcm orderOf = exponent G :=
+theorem lcm_orderOf_eq_exponent [Fintype G] : (Finset.univ : Finset G).lcm orderOf = exponent G :=
   by
   apply Nat.dvd_antisymm (lcm_order_of_dvd_exponent G)
   refine' exponent_dvd_of_forall_pow_eq_one G _ fun g => _
   obtain ⟨m, hm⟩ : orderOf g ∣ finset.univ.lcm orderOf := Finset.dvd_lcm (Finset.mem_univ g)
   rw [hm, pow_mul, pow_orderOf_eq_one, one_pow]
-#align monoid.lcm_order_eq_exponent Monoid.lcm_order_eq_exponent
-#align add_monoid.lcm_add_order_eq_exponent AddMonoid.lcm_addOrder_eq_exponent
+#align monoid.lcm_order_eq_exponent Monoid.lcm_orderOf_eq_exponent
+#align add_monoid.lcm_add_order_eq_exponent AddMonoid.lcm_addOrderOf_eq_exponent
 -/
 
 end Monoid

Mathbin/GroupTheory/Torsion.lean

@@ -163,7 +163,7 @@ theorem ExponentExists.isTorsion (h : ExponentExists G) : IsTorsion G := fun g =
       "The group exponent exists for any bounded additive torsion group."]
 theorem IsTorsion.exponentExists (tG : IsTorsion G)
     (bounded : (Set.range fun g : G => orderOf g).Finite) : ExponentExists G :=
-  exponentExists_iff_ne_zero.mpr <|
+  exponent_ne_zero.mpr <|
     (exponent_ne_zero_iff_range_orderOf_finite fun g => IsOfFinOrder.orderOf_pos (tG g)).mpr bounded
 #align is_torsion.exponent_exists IsTorsion.exponentExists
 #align is_add_torsion.exponent_exists IsAddTorsion.exponentExists
@@ -173,7 +173,7 @@ theorem IsTorsion.exponentExists (tG : IsTorsion G)
 /-- Finite groups are torsion groups. -/
 @[to_additive is_add_torsion_of_finite "Finite additive groups are additive torsion groups."]
 theorem isTorsion_of_finite [Finite G] : IsTorsion G :=
-  ExponentExists.isTorsion <| exponentExists_iff_ne_zero.mpr exponent_ne_zero_of_finite
+  ExponentExists.isTorsion <| exponent_ne_zero.mpr exponent_ne_zero_of_finite
 #align is_torsion_of_finite isTorsion_of_finite
 #align is_add_torsion_of_finite is_add_torsion_of_finite
 -/

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "3660a8f3955b041a7402b005bff03d7ed2eba7e9",
+   "rev": "1a7456e3362b211ee3a0aa4116a8fec19086f51b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "3660a8f3955b041a7402b005bff03d7ed2eba7e9",
+   "inputRev": "1a7456e3362b211ee3a0aa4116a8fec19086f51b",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "22fe986ea5142f5479719460e702e4d404fb7cbf",
+   "rev": "cbf36ddf824b03d88ada50c8f24481ea861da100",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "22fe986ea5142f5479719460e702e4d404fb7cbf",
+   "inputRev": "cbf36ddf824b03d88ada50c8f24481ea861da100",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "mathlib3port",

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-2024-02-17-08"
+def tag : String := "nightly-2024-02-18-08"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"22fe986ea5142f5479719460e702e4d404fb7cbf"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"cbf36ddf824b03d88ada50c8f24481ea861da100"
 
 @[default_target]
 lean_lib Mathbin where