bump to nightly-2024-04-23-08

mathlib commit leanprover-community/mathlib@65a1391

Mathbin/Algebra/BigOperators/Pi.lean

@@ -117,7 +117,7 @@ note [partially-applied ext lemmas]. -/
   to_additive
       "\nThis is used as the ext lemma instead of `add_monoid_hom.functions_ext` for reasons explained in\nnote [partially-applied ext lemmas]."]
 theorem MonoidHom.functions_ext' [Finite I] (M : Type _) [CommMonoid M] (g h : (∀ i, Z i) →* M)
-    (H : ∀ i, g.comp (MonoidHom.single Z i) = h.comp (MonoidHom.single Z i)) : g = h :=
+    (H : ∀ i, g.comp (MonoidHom.mulSingle Z i) = h.comp (MonoidHom.mulSingle Z i)) : g = h :=
   g.functions_ext M h fun i => MonoidHom.congr_fun (H i)
 #align monoid_hom.functions_ext' MonoidHom.functions_ext'
 #align add_monoid_hom.functions_ext' AddMonoidHom.functions_ext'

Mathbin/GroupTheory/Subsemigroup/Centralizer.lean → Mathbin/Algebra/Group/Centralizer.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Jireh Loreaux
 -/
-import GroupTheory.Subsemigroup.Center
+import Algebra.Group.Center
 import Algebra.GroupWithZero.Units.Lemmas
 
 #align_import group_theory.subsemigroup.centralizer from "leanprover-community/mathlib"@"cc67cd75b4e54191e13c2e8d722289a89e67e4fa"

Mathbin/Algebra/Group/Pi/Lemmas.lean

@@ -470,49 +470,49 @@ open Pi
 
 variable (f)
 
-#print OneHom.single /-
+#print OneHom.mulSingle /-
 /-- The one-preserving homomorphism including a single value
 into a dependent family of values, as functions supported at a point.
 
 This is the `one_hom` version of `pi.mul_single`. -/
 @[to_additive ZeroHom.single
       "The zero-preserving homomorphism including a single value\ninto a dependent family of values, as functions supported at a point.\n\nThis is the `zero_hom` version of `pi.single`."]
-def OneHom.single [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i)
+def OneHom.mulSingle [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i)
     where
   toFun := mulSingle i
   map_one' := mulSingle_one i
-#align one_hom.single OneHom.single
+#align one_hom.single OneHom.mulSingle
 #align zero_hom.single ZeroHom.single
 -/
 
-#print OneHom.single_apply /-
+#print OneHom.mulSingle_apply /-
 @[simp, to_additive]
-theorem OneHom.single_apply [∀ i, One <| f i] (i : I) (x : f i) :
-    OneHom.single f i x = mulSingle i x :=
+theorem OneHom.mulSingle_apply [∀ i, One <| f i] (i : I) (x : f i) :
+    OneHom.mulSingle f i x = mulSingle i x :=
   rfl
-#align one_hom.single_apply OneHom.single_apply
+#align one_hom.single_apply OneHom.mulSingle_apply
 #align zero_hom.single_apply ZeroHom.single_apply
 -/
 
-#print MonoidHom.single /-
+#print MonoidHom.mulSingle /-
 /-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
 as functions supported at a point.
 
 This is the `monoid_hom` version of `pi.mul_single`. -/
 @[to_additive
       "The additive monoid homomorphism including a single additive\nmonoid into a dependent family of additive monoids, as functions supported at a point.\n\nThis is the `add_monoid_hom` version of `pi.single`."]
-def MonoidHom.single [∀ i, MulOneClass <| f i] (i : I) : f i →* ∀ i, f i :=
-  { OneHom.single f i with map_mul' := mulSingle_op₂ (fun _ => (· * ·)) (fun _ => one_mul _) _ }
-#align monoid_hom.single MonoidHom.single
+def MonoidHom.mulSingle [∀ i, MulOneClass <| f i] (i : I) : f i →* ∀ i, f i :=
+  { OneHom.mulSingle f i with map_mul' := mulSingle_op₂ (fun _ => (· * ·)) (fun _ => one_mul _) _ }
+#align monoid_hom.single MonoidHom.mulSingle
 #align add_monoid_hom.single AddMonoidHom.single
 -/
 
-#print MonoidHom.single_apply /-
+#print MonoidHom.mulSingle_apply /-
 @[simp, to_additive]
-theorem MonoidHom.single_apply [∀ i, MulOneClass <| f i] (i : I) (x : f i) :
-    MonoidHom.single f i x = mulSingle i x :=
+theorem MonoidHom.mulSingle_apply [∀ i, MulOneClass <| f i] (i : I) (x : f i) :
+    MonoidHom.mulSingle f i x = mulSingle i x :=
   rfl
-#align monoid_hom.single_apply MonoidHom.single_apply
+#align monoid_hom.single_apply MonoidHom.mulSingle_apply
 #align add_monoid_hom.single_apply AddMonoidHom.single_apply
 -/
 
@@ -553,7 +553,7 @@ theorem Pi.mulSingle_inf [∀ i, SemilatticeInf (f i)] [∀ i, One (f i)] (i : I
 @[to_additive]
 theorem Pi.mulSingle_mul [∀ i, MulOneClass <| f i] (i : I) (x y : f i) :
     mulSingle i (x * y) = mulSingle i x * mulSingle i y :=
-  (MonoidHom.single f i).map_hMul x y
+  (MonoidHom.mulSingle f i).map_hMul x y
 #align pi.mul_single_mul Pi.mulSingle_mul
 #align pi.single_add Pi.single_add
 -/
@@ -562,17 +562,17 @@ theorem Pi.mulSingle_mul [∀ i, MulOneClass <| f i] (i : I) (x y : f i) :
 @[to_additive]
 theorem Pi.mulSingle_inv [∀ i, Group <| f i] (i : I) (x : f i) :
     mulSingle i x⁻¹ = (mulSingle i x)⁻¹ :=
-  (MonoidHom.single f i).map_inv x
+  (MonoidHom.mulSingle f i).map_inv x
 #align pi.mul_single_inv Pi.mulSingle_inv
 #align pi.single_neg Pi.single_neg
 -/
 
-#print Pi.single_div /-
+#print Pi.mulSingle_div /-
 @[to_additive]
-theorem Pi.single_div [∀ i, Group <| f i] (i : I) (x y : f i) :
+theorem Pi.mulSingle_div [∀ i, Group <| f i] (i : I) (x y : f i) :
     mulSingle i (x / y) = mulSingle i x / mulSingle i y :=
-  (MonoidHom.single f i).map_div x y
-#align pi.single_div Pi.single_div
+  (MonoidHom.mulSingle f i).map_div x y
+#align pi.single_div Pi.mulSingle_div
 #align pi.single_sub Pi.single_sub
 -/
 

Mathbin/Algebra/Lie/Weights/Basic.lean

@@ -247,22 +247,18 @@ theorem zero_weightSpace_eq_top_of_nilpotent [LieAlgebra.IsNilpotent R L] [IsNil
 #align lie_module.zero_weight_space_eq_top_of_nilpotent LieModule.zero_weightSpace_eq_top_of_nilpotent
 -/
 
-#print LieModule.IsWeight /-
 /-- Given a Lie module `M` of a Lie algebra `L`, a weight of `M` with respect to a nilpotent
 subalgebra `H ⊆ L` is a Lie character whose corresponding weight space is non-empty. -/
 def IsWeight (χ : LieCharacter R H) : Prop :=
   weightSpace M χ ≠ ⊥
 #align lie_module.is_weight LieModule.IsWeight
--/
 
-#print LieModule.isWeight_zero_of_nilpotent /-
 /-- For a non-trivial nilpotent Lie module over a nilpotent Lie algebra, the zero character is a
 weight with respect to the `⊤` Lie subalgebra. -/
-theorem isWeight_zero_of_nilpotent [Nontrivial M] [LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] :
+theorem isWeightZeroOfNilpotent [Nontrivial M] [LieAlgebra.IsNilpotent R L] [IsNilpotent R L M] :
     IsWeight (⊤ : LieSubalgebra R L) M 0 := by
   rw [is_weight, LieHom.coe_zero, zero_weight_space_eq_top_of_nilpotent]; exact top_ne_bot
-#align lie_module.is_weight_zero_of_nilpotent LieModule.isWeight_zero_of_nilpotent
--/
+#align lie_module.is_weight_zero_of_nilpotent LieModule.isWeightZeroOfNilpotent
 
 #print LieModule.isNilpotent_toEndomorphism_weightSpace_zero /-
 /-- A (nilpotent) Lie algebra acts nilpotently on the zero weight space of a Noetherian Lie
@@ -312,13 +308,11 @@ theorem zero_rootSpace_eq_top_of_nilpotent [h : IsNilpotent R L] :
 #align lie_algebra.zero_root_space_eq_top_of_nilpotent LieAlgebra.zero_rootSpace_eq_top_of_nilpotent
 -/
 
-#print LieAlgebra.IsRoot /-
 /-- A root of a Lie algebra `L` with respect to a nilpotent subalgebra `H ⊆ L` is a weight of `L`,
 regarded as a module of `H` via the adjoint action. -/
 abbrev IsRoot :=
   IsWeight H L
 #align lie_algebra.is_root LieAlgebra.IsRoot
--/
 
 #print LieAlgebra.rootSpace_comap_eq_weightSpace /-
 @[simp]

Mathbin/All.lean

@@ -1968,8 +1968,8 @@ import GroupTheory.Submonoid.Membership
 import GroupTheory.Submonoid.Operations
 import GroupTheory.Submonoid.Pointwise
 import GroupTheory.Subsemigroup.Basic
-import GroupTheory.Subsemigroup.Center
-import GroupTheory.Subsemigroup.Centralizer
+import Algebra.Group.Center
+import Algebra.Group.Centralizer
 import GroupTheory.Subsemigroup.Membership
 import GroupTheory.Subsemigroup.Operations
 import GroupTheory.Sylow

Mathbin/Data/Finset/NoncommProd.lean

@@ -466,7 +466,8 @@ theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
       x :=
   by
   ext i
-  apply (univ.noncomm_prod_map (fun i => MonoidHom.single M i (x i)) _ (Pi.evalMonoidHom M i)).trans
+  apply
+    (univ.noncomm_prod_map (fun i => MonoidHom.mulSingle M i (x i)) _ (Pi.evalMonoidHom M i)).trans
   rw [← insert_erase (mem_univ i), noncomm_prod_insert_of_not_mem' _ _ _ _ (not_mem_erase _ _),
     noncomm_prod_eq_pow_card, one_pow]
   · simp

Mathbin/GroupTheory/NoncommPiCoprod.lean

@@ -153,7 +153,7 @@ def noncommPiCoprodEquiv :
     where
   toFun ϕ := noncommPiCoprod ϕ.1 ϕ.2
   invFun f :=
-    ⟨fun i => f.comp (MonoidHom.single N i), fun i j hij x y =>
+    ⟨fun i => f.comp (MonoidHom.mulSingle N i), fun i j hij x y =>
       Commute.map (Pi.mulSingle_commute hij x y) f⟩
   left_inv ϕ := by ext; simp
   right_inv f := pi_ext fun i x => by simp

Mathbin/GroupTheory/Subgroup/Basic.lean

@@ -2268,8 +2268,8 @@ theorem pi_eq_bot_iff (H : ∀ i, Subgroup (f i)) : pi Set.univ H = ⊥ ↔ ∀
   simp only [eq_bot_iff_forall]
   constructor
   · intro h i x hx
-    have : MonoidHom.single f i x = 1 :=
-      h (MonoidHom.single f i x) ((mul_single_mem_pi i x).mpr fun _ => hx)
+    have : MonoidHom.mulSingle f i x = 1 :=
+      h (MonoidHom.mulSingle f i x) ((mul_single_mem_pi i x).mpr fun _ => hx)
     simpa using congr_fun this i
   · exact fun h x hx => funext fun i => h _ _ (hx i trivial)
 #align subgroup.pi_eq_bot_iff Subgroup.pi_eq_bot_iff

Mathbin/GroupTheory/Subgroup/Finite.lean

@@ -257,7 +257,7 @@ theorem pi_mem_of_mulSingle_mem [Finite η] [DecidableEq η] {H : Subgroup (∀
 @[to_additive
       "For finite index types, the `subgroup.pi` is generated by the embeddings of the\nadditive groups."]
 theorem pi_le_iff [DecidableEq η] [Finite η] {H : ∀ i, Subgroup (f i)} {J : Subgroup (∀ i, f i)} :
-    pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.single f i) (H i) ≤ J :=
+    pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J :=
   by
   constructor
   · rintro h i _ ⟨x, hx, rfl⟩; apply h; simpa using hx

Mathbin/GroupTheory/Submonoid/Center.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import GroupTheory.Submonoid.Operations
-import GroupTheory.Subsemigroup.Center
+import Algebra.Group.Center
 
 #align_import group_theory.submonoid.center from "leanprover-community/mathlib"@"baba818b9acea366489e8ba32d2cc0fcaf50a1f7"
 

Mathbin/GroupTheory/Submonoid/Centralizer.lean

@@ -3,7 +3,7 @@ Copyright (c) 2021 Thomas Browning. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
-import GroupTheory.Subsemigroup.Centralizer
+import Algebra.Group.Centralizer
 import GroupTheory.Submonoid.Center
 
 #align_import group_theory.submonoid.centralizer from "leanprover-community/mathlib"@"cc67cd75b4e54191e13c2e8d722289a89e67e4fa"

Mathbin/RingTheory/NonUnitalSubsemiring/Basic.lean

@@ -8,7 +8,7 @@ import Algebra.Ring.Prod
 import Data.Set.Finite
 import GroupTheory.Submonoid.Membership
 import GroupTheory.Subsemigroup.Membership
-import GroupTheory.Subsemigroup.Centralizer
+import Algebra.Group.Centralizer
 
 #align_import ring_theory.non_unital_subsemiring.basic from "leanprover-community/mathlib"@"b915e9392ecb2a861e1e766f0e1df6ac481188ca"
 

lake-manifest.json

@@ -58,19 +58,19 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f26580092e3ee3285dfa69b9e43e35ba1daa05fa",
+   "rev": "5b96848cc28fea8b782392a020db7a20824d9409",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "f26580092e3ee3285dfa69b9e43e35ba1daa05fa",
+   "inputRev": "5b96848cc28fea8b782392a020db7a20824d9409",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean3port.git",
    "type": "git",
    "subDir": null,
-   "rev": "4faa903f7d3b951335b23c8112576e0363c1a5fd",
+   "rev": "df4fde5e5167e06404cc5ca52c01444dadd6b96c",
    "name": "lean3port",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "4faa903f7d3b951335b23c8112576e0363c1a5fd",
+   "inputRev": "df4fde5e5167e06404cc5ca52c01444dadd6b96c",
    "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-04-21-08"
+def tag : String := "nightly-2024-04-23-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"@"4faa903f7d3b951335b23c8112576e0363c1a5fd"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"df4fde5e5167e06404cc5ca52c01444dadd6b96c"
 
 @[default_target]
 lean_lib Mathbin where