chore: Rename a few lemmas about Pi.mulSingle (#12317)

Before this PR, the `MonoidHom` version of `Pi.mulSingle` was called `MonoidHom.single` for brevity; but this is confusing when contrasted with `MulHom.single` which is about `Pi.single`.

After this PR, the name is `MonoidHom.mulSingle`.

Also fix the name of `Pi.single_div` since it is about `Pi.mulSingle` (and we don't have the lemma that would be called `Pi.single_div`).

Author: YaelDillies

Mathlib/Algebra/BigOperators/Pi.lean

@@ -104,7 +104,7 @@ note [partially-applied ext lemmas]. -/
       "\nThis is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons
       explained in note [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 => DFunLike.congr_fun (H i)
 #align monoid_hom.functions_ext' MonoidHom.functions_ext'
 #align add_monoid_hom.functions_ext' AddMonoidHom.functions_ext'

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -271,17 +271,16 @@ This is the `OneHom` version of `Pi.mulSingle`. -/
       as functions supported at a point.
 
       This is the `ZeroHom` version of `Pi.single`."]
-def OneHom.single [∀ i, One <| f i] (i : I) : OneHom (f i) (∀ i, f i) where
+nonrec 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
 
 @[to_additive (attr := simp)]
-theorem OneHom.single_apply [∀ i, One <| f i] (i : I) (x : f i) :
-    OneHom.single f i x = mulSingle i x :=
-  rfl
-#align one_hom.single_apply OneHom.single_apply
+theorem OneHom.mulSingle_apply [∀ i, One <| f i] (i : I) (x : f i) :
+    mulSingle f i x = Pi.mulSingle i x := rfl
+#align one_hom.single_apply OneHom.mulSingle_apply
 #align zero_hom.single_apply ZeroHom.single_apply
 
 /-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
@@ -293,16 +292,16 @@ This is the `MonoidHom` version of `Pi.mulSingle`. -/
       of additive monoids, as functions supported at a point.
 
       This is the `AddMonoidHom` 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
 
 @[to_additive (attr := simp)]
-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) :
+    mulSingle f i x = Pi.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
 
 /-- The multiplicative homomorphism including a single `MulZeroClass`
@@ -335,22 +334,22 @@ 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_mul x y
+  (MonoidHom.mulSingle f i).map_mul x y
 #align pi.mul_single_mul Pi.mulSingle_mul
 #align pi.single_add Pi.single_add
 
 @[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
 
 @[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
 
 theorem Pi.single_mul [∀ i, MulZeroClass <| f i] (i : I) (x y : f i) :

Mathlib/Data/Finset/NoncommProd.lean

@@ -462,7 +462,8 @@ theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
     (univ.noncommProd (fun i => Pi.mulSingle i (x i)) fun i _ j _ _ =>
         Pi.mulSingle_apply_commute x i j) = x := by
   ext i
-  apply (univ.noncommProd_map (fun i => MonoidHom.single M i (x i)) ?a (Pi.evalMonoidHom M i)).trans
+  apply (univ.noncommProd_map (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
+    (Pi.evalMonoidHom M i)).trans
   case a =>
     intro i _ j _ _
     exact Pi.mulSingle_apply_commute x i j
@@ -472,10 +473,10 @@ theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) :
   · intro j _; dsimp
   · rw [noncommProd_insert_of_not_mem _ _ _ _ (not_mem_erase _ _),
       noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one]
-    simp only [MonoidHom.single_apply, ne_eq, Pi.mulSingle_eq_same]
+    simp only [MonoidHom.mulSingle_apply, ne_eq, Pi.mulSingle_eq_same]
     · intro j hj
       simp? at hj says simp only [mem_erase, ne_eq, mem_univ, and_true] at hj
-      simp only [MonoidHom.single_apply, Pi.mulSingle, Function.update, Eq.ndrec, Pi.one_apply,
+      simp only [MonoidHom.mulSingle_apply, Pi.mulSingle, Function.update, Eq.ndrec, Pi.one_apply,
         ne_eq, dite_eq_right_iff]
       intro h
       simp [*] at *

Mathlib/GroupTheory/NoncommPiCoprod.lean

@@ -148,13 +148,13 @@ 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 only [coe_comp, Function.comp_apply, single_apply, noncommPiCoprod_mulSingle]
+    simp only [coe_comp, Function.comp_apply, mulSingle_apply, noncommPiCoprod_mulSingle]
   right_inv f := pi_ext fun i x => by
-    simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, single_apply]
+    simp only [noncommPiCoprod_mulSingle, coe_comp, Function.comp_apply, mulSingle_apply]
 #align monoid_hom.noncomm_pi_coprod_equiv MonoidHom.noncommPiCoprodEquiv
 #align add_monoid_hom.noncomm_pi_coprod_equiv AddMonoidHom.noncommPiCoprodEquiv
 

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -1897,8 +1897,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) ((mulSingle_mem_pi i x).mpr fun _ => hx)
+      have : MonoidHom.mulSingle f i x = 1 :=
+        h (MonoidHom.mulSingle f i x) ((mulSingle_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

Mathlib/GroupTheory/Subgroup/Finite.lean

@@ -243,7 +243,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
  additive 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 := by
+    pi univ H ≤ J ↔ ∀ i : η, map (MonoidHom.mulSingle f i) (H i) ≤ J := by
   constructor
   · rintro h i _ ⟨x, hx, rfl⟩
     apply h

Mathlib/Probability/Moments.lean

@@ -61,7 +61,7 @@ def centralMoment (X : Ω → ℝ) (p : ℕ) (μ : Measure Ω) : ℝ := by
 @[simp]
 theorem moment_zero (hp : p ≠ 0) : moment 0 p μ = 0 := by
   simp only [moment, hp, zero_pow, Ne, not_false_iff, Pi.zero_apply, integral_const,
-    smul_eq_mul, mul_zero]
+    smul_eq_mul, mul_zero, integral_zero]
 #align probability_theory.moment_zero ProbabilityTheory.moment_zero
 
 @[simp]

Mathlib/RingTheory/PiTensorProduct.lean

@@ -188,7 +188,7 @@ The map `Aᵢ ⟶ ⨂ᵢ Aᵢ` given by `a ↦ 1 ⊗ ... ⊗ a ⊗ 1 ⊗ ...`
 -/
 @[simps]
 def singleAlgHom [DecidableEq ι] (i : ι) : A i →ₐ[R] ⨂[R] i, A i where
-  toFun a := tprod R (MonoidHom.single _ i a)
+  toFun a := tprod R (MonoidHom.mulSingle _ i a)
   map_one' := by simp only [_root_.map_one]; rfl
   map_mul' a a' := by simp
   map_zero' := MultilinearMap.map_update_zero _ _ _