bump to nightly-2023-03-11-16

mathlib commit leanprover-community/mathlib@3180fab

Mathbin/Algebra/Algebra/Bilinear.lean

@@ -221,7 +221,7 @@ def LinearMap.NonUnitalAlgHom.lmul : A →ₙₐ[R] End R A :=
       exact mul_assoc a b c
     map_zero' := by
       ext a
-      exact zero_mul a }
+      exact MulZeroClass.zero_mul a }
 #align non_unital_alg_hom.lmul LinearMap.NonUnitalAlgHom.lmul
 
 variable {R A}
@@ -305,7 +305,7 @@ def LinearMap.Algebra.lmul : A →ₐ[R] End R A :=
       exact mul_assoc a b c
     map_zero' := by
       ext a
-      exact zero_mul a
+      exact MulZeroClass.zero_mul a
     commutes' := by
       intro r
       ext a

Mathbin/Algebra/Algebra/Operations.lean

@@ -1025,7 +1025,7 @@ instance : Div (Submodule R A) :=
   ⟨fun I J =>
     { carrier := { x | ∀ y ∈ J, x * y ∈ I }
       zero_mem' := fun y hy => by
-        rw [zero_mul]
+        rw [MulZeroClass.zero_mul]
         apply Submodule.zero_mem
       add_mem' := fun a b ha hb y hy => by
         rw [add_mul]

Mathbin/Algebra/Algebra/Unitization.lean

@@ -379,7 +379,8 @@ theorem inl_one [One R] [Zero A] : (inl 1 : Unitization R A) = 1 :=
 theorem inl_mul [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r₁ r₂ : R) :
     (inl (r₁ * r₂) : Unitization R A) = inl r₁ * inl r₂ :=
   ext rfl <|
-    show (0 : A) = r₁ • (0 : A) + r₂ • 0 + 0 * 0 by simp only [smul_zero, add_zero, mul_zero]
+    show (0 : A) = r₁ • (0 : A) + r₂ • 0 + 0 * 0 by
+      simp only [smul_zero, add_zero, MulZeroClass.mul_zero]
 #align unitization.inl_mul Unitization.inl_mul
 
 theorem inl_mul_inl [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r₁ r₂ : R) :
@@ -396,22 +397,24 @@ variable (R)
 @[simp]
 theorem coe_mul [Semiring R] [AddCommMonoid A] [Mul A] [SMulWithZero R A] (a₁ a₂ : A) :
     (↑(a₁ * a₂) : Unitization R A) = a₁ * a₂ :=
-  ext (mul_zero _).symm <|
+  ext (MulZeroClass.mul_zero _).symm <|
     show a₁ * a₂ = (0 : R) • a₂ + (0 : R) • a₁ + a₁ * a₂ by simp only [zero_smul, zero_add]
 #align unitization.coe_mul Unitization.coe_mul
 
 end
 
 theorem inl_mul_coe [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
     (a : A) : (inl r * a : Unitization R A) = ↑(r • a) :=
-  ext (mul_zero r) <|
-    show r • a + (0 : R) • 0 + 0 * a = r • a by rw [smul_zero, add_zero, zero_mul, add_zero]
+  ext (MulZeroClass.mul_zero r) <|
+    show r • a + (0 : R) • 0 + 0 * a = r • a by
+      rw [smul_zero, add_zero, MulZeroClass.zero_mul, add_zero]
 #align unitization.inl_mul_coe Unitization.inl_mul_coe
 
 theorem coe_mul_inl [Semiring R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] (r : R)
     (a : A) : (a * inl r : Unitization R A) = ↑(r • a) :=
-  ext (zero_mul r) <|
-    show (0 : R) • 0 + r • a + a * 0 = r • a by rw [smul_zero, zero_add, mul_zero, add_zero]
+  ext (MulZeroClass.zero_mul r) <|
+    show (0 : R) • 0 + r • a + a * 0 = r • a by
+      rw [smul_zero, zero_add, MulZeroClass.mul_zero, add_zero]
 #align unitization.coe_mul_inl Unitization.coe_mul_inl
 
 instance mulOneClass [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] :
@@ -421,25 +424,25 @@ instance mulOneClass [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction
     one_mul := fun x =>
       ext (one_mul x.1) <|
         show (1 : R) • x.2 + x.1 • 0 + 0 * x.2 = x.2 by
-          rw [one_smul, smul_zero, add_zero, zero_mul, add_zero]
+          rw [one_smul, smul_zero, add_zero, MulZeroClass.zero_mul, add_zero]
     mul_one := fun x =>
       ext (mul_one x.1) <|
         show (x.1 • 0 : A) + (1 : R) • x.2 + x.2 * 0 = x.2 by
-          rw [smul_zero, zero_add, one_smul, mul_zero, add_zero] }
+          rw [smul_zero, zero_add, one_smul, MulZeroClass.mul_zero, add_zero] }
 #align unitization.mul_one_class Unitization.mulOneClass
 
 instance [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] :
     NonAssocSemiring (Unitization R A) :=
   { Unitization.mulOneClass,
     Unitization.addCommMonoid with
     zero_mul := fun x =>
-      ext (zero_mul x.1) <|
+      ext (MulZeroClass.zero_mul x.1) <|
         show (0 : R) • x.2 + x.1 • 0 + 0 * x.2 = 0 by
-          rw [zero_smul, zero_add, smul_zero, zero_mul, add_zero]
+          rw [zero_smul, zero_add, smul_zero, MulZeroClass.zero_mul, add_zero]
     mul_zero := fun x =>
-      ext (mul_zero x.1) <|
+      ext (MulZeroClass.mul_zero x.1) <|
         show (x.1 • 0 : A) + (0 : R) • x.2 + x.2 * 0 = 0 by
-          rw [smul_zero, zero_add, zero_smul, mul_zero, add_zero]
+          rw [smul_zero, zero_add, zero_smul, MulZeroClass.mul_zero, add_zero]
     left_distrib := fun x₁ x₂ x₃ =>
       ext (mul_add x₁.1 x₂.1 x₃.1) <|
         show
@@ -661,9 +664,10 @@ def lift : (A →ₙₐ[R] C) ≃ (Unitization R A →ₐ[R] C)
       map_mul' := fun x y => by
         induction x using Unitization.ind
         induction y using Unitization.ind
-        simp only [mul_add, add_mul, coe_mul, fst_add, fst_mul, fst_inl, fst_coe, mul_zero,
-          add_zero, zero_mul, map_mul, snd_add, snd_mul, snd_inl, smul_zero, snd_coe, zero_add,
-          φ.map_add, φ.map_smul, φ.map_mul, zero_smul, zero_add]
+        simp only [mul_add, add_mul, coe_mul, fst_add, fst_mul, fst_inl, fst_coe,
+          MulZeroClass.mul_zero, add_zero, MulZeroClass.zero_mul, map_mul, snd_add, snd_mul,
+          snd_inl, smul_zero, snd_coe, zero_add, φ.map_add, φ.map_smul, φ.map_mul, zero_smul,
+          zero_add]
         rw [← Algebra.commutes _ (φ x_a)]
         simp only [Algebra.algebraMap_eq_smul_one, smul_one_mul, add_assoc]
       map_zero' := by simp only [fst_zero, map_zero, snd_zero, φ.map_zero, add_zero]

Mathbin/Algebra/Associated.lean

@@ -329,7 +329,7 @@ Case conversion may be inaccurate. Consider using '#align not_irreducible_zero n
 @[simp]
 theorem not_irreducible_zero [MonoidWithZero α] : ¬Irreducible (0 : α)
   | ⟨hn0, h⟩ =>
-    have : IsUnit (0 : α) ∨ IsUnit (0 : α) := h 0 0 (mul_zero 0).symm
+    have : IsUnit (0 : α) ∨ IsUnit (0 : α) := h 0 0 (MulZeroClass.mul_zero 0).symm
     this.elim hn0 hn0
 #align not_irreducible_zero not_irreducible_zero
 
@@ -903,7 +903,7 @@ theorem associated_of_dvd_dvd [CancelMonoidWithZero α] {a b : α} (hab : a ∣
   · simp_all
   have hac0 : a * c ≠ 0 := by
     intro con
-    rw [Con, zero_mul] at a_eq
+    rw [Con, MulZeroClass.zero_mul] at a_eq
     apply ha0 a_eq
   have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
   have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
@@ -1590,15 +1590,15 @@ instance : CommMonoidWithZero (Associates α) :=
     zero_mul := by
       rintro ⟨a⟩
       show Associates.mk (0 * a) = Associates.mk 0
-      rw [zero_mul]
+      rw [MulZeroClass.zero_mul]
     mul_zero := by
       rintro ⟨a⟩
       show Associates.mk (a * 0) = Associates.mk 0
-      rw [mul_zero] }
+      rw [MulZeroClass.mul_zero] }
 
 instance : OrderTop (Associates α) where
   top := 0
-  le_top a := ⟨0, (mul_zero a).symm⟩
+  le_top a := ⟨0, (MulZeroClass.mul_zero a).symm⟩
 
 instance : BoundedOrder (Associates α) :=
   { Associates.orderTop, Associates.orderBot with }

Mathbin/Algebra/BigOperators/Basic.lean

@@ -2729,7 +2729,7 @@ Case conversion may be inaccurate. Consider using '#align finset.prod_eq_zero Fi
 theorem prod_eq_zero (ha : a ∈ s) (h : f a = 0) : (∏ x in s, f x) = 0 :=
   by
   haveI := Classical.decEq α
-  rw [← prod_erase_mul _ _ ha, h, mul_zero]
+  rw [← prod_erase_mul _ _ ha, h, MulZeroClass.mul_zero]
 #align finset.prod_eq_zero Finset.prod_eq_zero
 
 /- warning: finset.prod_boole -> Finset.prod_boole is a dubious translation:

Mathbin/Algebra/Category/Module/Adjunctions.lean

@@ -229,8 +229,8 @@ instance categoryFree : Category (Free R C)
     dsimp
     -- This imitates the proof of associativity for `monoid_algebra`.
     simp only [sum_sum_index, sum_single_index, single_zero, single_add, eq_self_iff_true,
-      forall_true_iff, forall₃_true_iff, add_mul, mul_add, category.assoc, mul_assoc, zero_mul,
-      mul_zero, sum_zero, sum_add]
+      forall_true_iff, forall₃_true_iff, add_mul, mul_add, category.assoc, mul_assoc,
+      MulZeroClass.zero_mul, MulZeroClass.mul_zero, sum_zero, sum_add]
 #align category_theory.category_Free CategoryTheory.categoryFree
 
 namespace Free

Mathbin/Algebra/Category/Ring/Constructions.lean

@@ -149,7 +149,7 @@ instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRin
     rw [← f.map_one, ← f.map_zero]
     congr
   replace e : 0 * x = 1 * x := congr_arg (fun a => a * x) e
-  rw [one_mul, zero_mul, ← f.map_zero] at e
+  rw [one_mul, MulZeroClass.zero_mul, ← f.map_zero] at e
   exact e
 #align CommRing.CommRing_has_strict_terminal_objects CommRingCat.commRingCat_hasStrictTerminalObjects
 

Mathbin/Algebra/Category/Ring/FilteredColimits.lean

@@ -78,13 +78,13 @@ instance colimitSemiring : Semiring R :=
       apply Quot.inductionOn x; clear x; intro x
       cases' x with j x
       erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
-      rw [CategoryTheory.Functor.map_id, id_apply, id_apply, mul_zero x]
+      rw [CategoryTheory.Functor.map_id, id_apply, id_apply, MulZeroClass.mul_zero x]
       rfl
     zero_mul := fun x => by
       apply Quot.inductionOn x; clear x; intro x
       cases' x with j x
       erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
-      rw [CategoryTheory.Functor.map_id, id_apply, id_apply, zero_mul x]
+      rw [CategoryTheory.Functor.map_id, id_apply, id_apply, MulZeroClass.zero_mul x]
       rfl
     left_distrib := fun x y z => by
       apply Quot.induction_on₃ x y z; clear x y z; intro x y z

Mathbin/Algebra/CharP/Basic.lean

@@ -97,12 +97,13 @@ theorem CharP.exists [NonAssocSemiring R] : ∃ p, CharP R p :=
                   ⟨by
                     rwa [← Nat.mod_add_div x (Nat.find (not_forall.1 H)), Nat.cast_add,
                       Nat.cast_mul,
-                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul,
-                      add_zero] at H1,
+                      of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
+                      MulZeroClass.zero_mul, add_zero] at H1,
                     H2⟩)),
           fun H1 => by
           rw [← Nat.mul_div_cancel' H1, Nat.cast_mul,
-            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)), zero_mul]⟩⟩⟩
+            of_not_not (not_not_of_not_imp <| Nat.find_spec (not_forall.1 H)),
+            MulZeroClass.zero_mul]⟩⟩⟩
 #align char_p.exists CharP.exists
 
 theorem CharP.existsUnique [NonAssocSemiring R] : ∃! p, CharP R p :=
@@ -522,7 +523,7 @@ instance (priority := 100) [CharP R 1] : Subsingleton R :=
       r = 1 * r := by rw [one_mul]
       _ = (1 : ℕ) * r := by rw [Nat.cast_one]
       _ = 0 * r := by rw [CharP.cast_eq_zero]
-      _ = 0 := by rw [zero_mul]
+      _ = 0 := by rw [MulZeroClass.zero_mul]
 
 
 theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
@@ -594,13 +595,14 @@ theorem charP_of_ne_zero (hn : Fintype.card R = n) (hR : ∀ i < n, (i : R) = 0
       intro k
       constructor
       · intro h
-        rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
+        rw [← Nat.mod_add_div k n, Nat.cast_add, Nat.cast_mul, H, MulZeroClass.zero_mul,
+          add_zero] at h
         rw [Nat.dvd_iff_mod_eq_zero]
         apply hR _ (Nat.mod_lt _ _) h
         rw [← hn, Fintype.card_pos_iff]
         exact ⟨0⟩
       · rintro ⟨k, rfl⟩
-        rw [Nat.cast_mul, H, zero_mul] }
+        rw [Nat.cast_mul, H, MulZeroClass.zero_mul] }
 #align char_p_of_ne_zero charP_of_ne_zero
 
 theorem charP_of_prime_pow_injective (R) [Ring R] [Fintype R] (p : ℕ) [hp : Fact p.Prime] (n : ℕ)

Mathbin/Algebra/CharP/CharAndCard.lean

@@ -39,14 +39,14 @@ theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type _) [CommRing R] (p
     have h₄ := mt (CharP.int_cast_eq_zero_iff R (ringChar R) q).mp
     apply_fun (coe : ℕ → R)  at hq
     apply_fun (· * ·) a  at hq
-    rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq
+    rw [Nat.cast_mul, hch, MulZeroClass.mul_zero, ← mul_assoc, ha, one_mul] at hq
     norm_cast  at h₄
     exact h₄ h₃ hq.symm
   · intro h
     rcases(hp.coprime_iff_not_dvd.mpr h).IsCoprime with ⟨a, b, hab⟩
     apply_fun (coe : ℤ → R)  at hab
     push_cast at hab
-    rw [hch, mul_zero, add_zero, mul_comm] at hab
+    rw [hch, MulZeroClass.mul_zero, add_zero, mul_comm] at hab
     exact isUnit_of_mul_eq_one (p : R) a hab
 #align is_unit_iff_not_dvd_char_of_ring_char_ne_zero isUnit_iff_not_dvd_char_of_ringChar_ne_zero
 
@@ -75,7 +75,7 @@ theorem prime_dvd_char_iff_dvd_card {R : Type _} [CommRing R] [Fintype R] (p : 
   rw [hr, nsmul_eq_mul] at hr₁
   rcases IsUnit.exists_left_inv ((isUnit_iff_not_dvd_char R p).mpr h₀) with ⟨u, hu⟩
   apply_fun (· * ·) u  at hr₁
-  rw [mul_zero, ← mul_assoc, hu, one_mul] at hr₁
+  rw [MulZeroClass.mul_zero, ← mul_assoc, hu, one_mul] at hr₁
   exact
     mt add_monoid.order_of_eq_one_iff.mpr (ne_of_eq_of_ne hr (Nat.Prime.ne_one (Fact.out p.prime)))
       hr₁

Mathbin/Algebra/ContinuedFractions/Computation/Approximations.lean

@@ -622,7 +622,7 @@ theorem abs_sub_convergents_le' {b : K}
   -- to consider the case `(generalized_continued_fraction.of v).denominators n = 0`.
   rcases zero_le_of_denom.eq_or_gt with
     ((hB : (GeneralizedContinuedFraction.of v).denominators n = 0) | hB)
-  · simp only [hB, mul_zero, zero_mul, div_zero]
+  · simp only [hB, MulZeroClass.mul_zero, MulZeroClass.zero_mul, div_zero]
   · apply one_div_le_one_div_of_le
     · have : 0 < b := zero_lt_one.trans_le (of_one_le_nth_part_denom nth_part_denom_eq)
       apply_rules [mul_pos]

Mathbin/Algebra/CubicDiscriminant.lean

@@ -141,23 +141,23 @@ theorem toPoly_injective (P Q : Cubic R) : P.toPoly = Q.toPoly ↔ P = Q :=
 #align cubic.to_poly_injective Cubic.toPoly_injective
 
 theorem of_a_eq_zero (ha : P.a = 0) : P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d := by
-  rw [to_poly, ha, C_0, zero_mul, zero_add]
+  rw [to_poly, ha, C_0, MulZeroClass.zero_mul, zero_add]
 #align cubic.of_a_eq_zero Cubic.of_a_eq_zero
 
 theorem of_a_eq_zero' : toPoly ⟨0, b, c, d⟩ = C b * X ^ 2 + C c * X + C d :=
   of_a_eq_zero rfl
 #align cubic.of_a_eq_zero' Cubic.of_a_eq_zero'
 
 theorem of_b_eq_zero (ha : P.a = 0) (hb : P.b = 0) : P.toPoly = C P.c * X + C P.d := by
-  rw [of_a_eq_zero ha, hb, C_0, zero_mul, zero_add]
+  rw [of_a_eq_zero ha, hb, C_0, MulZeroClass.zero_mul, zero_add]
 #align cubic.of_b_eq_zero Cubic.of_b_eq_zero
 
 theorem of_b_eq_zero' : toPoly ⟨0, 0, c, d⟩ = C c * X + C d :=
   of_b_eq_zero rfl rfl
 #align cubic.of_b_eq_zero' Cubic.of_b_eq_zero'
 
 theorem of_c_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) : P.toPoly = C P.d := by
-  rw [of_b_eq_zero ha hb, hc, C_0, zero_mul, zero_add]
+  rw [of_b_eq_zero ha hb, hc, C_0, MulZeroClass.zero_mul, zero_add]
 #align cubic.of_c_eq_zero Cubic.of_c_eq_zero
 
 theorem of_c_eq_zero' : toPoly ⟨0, 0, 0, d⟩ = C d :=

Mathbin/Algebra/DirectLimit.lean

@@ -589,7 +589,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
         _⟩
     rw [(restriction _).map_mul, (FreeCommRing.lift _).map_mul, ←
       of.zero_exact_aux2 G f' hyt hj this hjk (Set.subset_union_right (↑s) t), iht,
-      (f' j k hjk).map_zero, mul_zero]
+      (f' j k hjk).map_zero, MulZeroClass.mul_zero]
 #align ring.direct_limit.of.zero_exact_aux Ring.DirectLimit.of.zero_exact_aux
 
 /-- A component that corresponds to zero in the direct limit is already zero in some

Mathbin/Algebra/DirectSum/Internal.lean

@@ -96,19 +96,23 @@ namespace SetLike
 instance gnonUnitalNonAssocSemiring [Add ι] [NonUnitalNonAssocSemiring R] [SetLike σ R]
     [AddSubmonoidClass σ R] (A : ι → σ) [SetLike.GradedMul A] :
     DirectSum.GnonUnitalNonAssocSemiring fun i => A i :=
-  { SetLike.gMul A with
-    mul_zero := fun i j _ => Subtype.ext (mul_zero _)
-    zero_mul := fun i j _ => Subtype.ext (zero_mul _)
+  {
+    SetLike.gMul
+      A with
+    mul_zero := fun i j _ => Subtype.ext (MulZeroClass.mul_zero _)
+    zero_mul := fun i j _ => Subtype.ext (MulZeroClass.zero_mul _)
     mul_add := fun i j _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun i j _ _ _ => Subtype.ext (add_mul _ _ _) }
 #align set_like.gnon_unital_non_assoc_semiring SetLike.gnonUnitalNonAssocSemiring
 
 /-- Build a `gsemiring` instance for a collection of additive submonoids. -/
 instance gsemiring [AddMonoid ι] [Semiring R] [SetLike σ R] [AddSubmonoidClass σ R] (A : ι → σ)
     [SetLike.GradedMonoid A] : DirectSum.Gsemiring fun i => A i :=
-  { SetLike.gMonoid A with
-    mul_zero := fun i j _ => Subtype.ext (mul_zero _)
-    zero_mul := fun i j _ => Subtype.ext (zero_mul _)
+  {
+    SetLike.gMonoid
+      A with
+    mul_zero := fun i j _ => Subtype.ext (MulZeroClass.mul_zero _)
+    zero_mul := fun i j _ => Subtype.ext (MulZeroClass.zero_mul _)
     mul_add := fun i j _ _ _ => Subtype.ext (mul_add _ _ _)
     add_mul := fun i j _ _ _ => Subtype.ext (add_mul _ _ _)
     natCast := fun n => ⟨n, SetLike.nat_cast_mem_graded _ _⟩
@@ -191,12 +195,12 @@ theorem coe_of_mul_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r
     rw [coe_mul_apply_eq_dfinsupp_sum]
     apply (Dfinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, zero_mul, if_t_t]
+    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.zero_mul, if_t_t]
       exact Dfinsupp.sum_zero
     simp_rw [Dfinsupp.sum, H, Finset.sum_ite_eq']
     split_ifs
     rfl
-    rw [dfinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, mul_zero]
+    rw [dfinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, MulZeroClass.mul_zero]
 #align direct_sum.coe_of_mul_apply_aux DirectSum.coe_of_mul_apply_aux
 
 theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i, A i) {i : ι}
@@ -205,12 +209,12 @@ theorem coe_mul_of_apply_aux [AddMonoid ι] [SetLike.GradedMonoid A] (r : ⨁ i,
     rw [coe_mul_apply_eq_dfinsupp_sum, Dfinsupp.sum_comm]
     apply (Dfinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, mul_zero, if_t_t]
+    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.mul_zero, if_t_t]
       exact Dfinsupp.sum_zero
     simp_rw [Dfinsupp.sum, H, Finset.sum_ite_eq']
     split_ifs
     rfl
-    rw [dfinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, zero_mul]
+    rw [dfinsupp.not_mem_support_iff.mp h, ZeroMemClass.coe_zero, MulZeroClass.zero_mul]
 #align direct_sum.coe_mul_of_apply_aux DirectSum.coe_mul_of_apply_aux
 
 theorem coe_of_mul_apply_add [AddLeftCancelMonoid ι] [SetLike.GradedMonoid A] {i : ι} (r : A i)
@@ -237,7 +241,7 @@ theorem coe_of_mul_apply_of_not_le {i : ι} (r : A i) (r' : ⨁ i, A i) (n : ι)
     rw [coe_mul_apply_eq_dfinsupp_sum]
     apply (Dfinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, zero_mul, if_t_t]
+    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.zero_mul, if_t_t]
       exact Dfinsupp.sum_zero
     · rw [Dfinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
       exact h ((self_le_add_right i x).trans_eq H)
@@ -249,7 +253,7 @@ theorem coe_mul_of_apply_of_not_le (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι)
     rw [coe_mul_apply_eq_dfinsupp_sum, Dfinsupp.sum_comm]
     apply (Dfinsupp.sum_single_index _).trans
     swap
-    · simp_rw [ZeroMemClass.coe_zero, mul_zero, if_t_t]
+    · simp_rw [ZeroMemClass.coe_zero, MulZeroClass.mul_zero, if_t_t]
       exact Dfinsupp.sum_zero
     · rw [Dfinsupp.sum, Finset.sum_ite_of_false _ _ fun x _ H => _, Finset.sum_const_zero]
       exact h ((self_le_add_left i x).trans_eq H)

Mathbin/Algebra/DirectSum/Ring.lean

@@ -660,8 +660,8 @@ variable (ι)
 instance NonUnitalNonAssocSemiring.directSumGnonUnitalNonAssocSemiring {R : Type _} [AddMonoid ι]
     [NonUnitalNonAssocSemiring R] : DirectSum.GnonUnitalNonAssocSemiring fun i : ι => R :=
   { Mul.gMul ι with
-    mul_zero := fun i j => mul_zero
-    zero_mul := fun i j => zero_mul
+    mul_zero := fun i j => MulZeroClass.mul_zero
+    zero_mul := fun i j => MulZeroClass.zero_mul
     mul_add := fun i j => mul_add
     add_mul := fun i j => add_mul }
 #align non_unital_non_assoc_semiring.direct_sum_gnon_unital_non_assoc_semiring NonUnitalNonAssocSemiring.directSumGnonUnitalNonAssocSemiring