refactor: do not allow nsmul and zsmul to default automatically (#…

…6262)

This PR removes the default values for `nsmul` and `zsmul`, forcing the user to populate them manually.
The previous behavior can be obtained by writing `nsmul := nsmulRec` and `zsmul := zsmulRec`, which is now in the docstring for these fields.

The motivation here is to make it more obvious when module diamonds are being introduced, or at least where they might be hiding; you can now simply search for `nsmulRec` in the source code.

Arguably we should do the same thing for `intCast`, `natCast`, `pow`, and `zpow` too, but diamonds are less common in those fields, so I'll leave them to a subsequent PR.



Co-authored-by: Matthew Ballard <matt@mrb.email>

Counterexamples/Monic_nonRegular.lean

@@ -71,7 +71,8 @@ instance : CommSemiring N₃ :=
     left_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
     right_distrib := by rintro ⟨⟩ ⟨⟩ ⟨⟩ <;> rfl
     zero_mul := by rintro ⟨⟩ <;> rfl
-    mul_zero := by rintro ⟨⟩ <;> rfl }
+    mul_zero := by rintro ⟨⟩ <;> rfl
+    nsmul := nsmulRec }
 
 theorem X_add_two_mul_X_add_two : (X + C 2 : N₃[X]) * (X + C 2) = (X + C 2) * (X + C 3) := by
   simp only [mul_add, add_mul, X_mul, add_assoc]

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -180,14 +180,17 @@ instance : LinearOrder F :=
 theorem z01 : (0 : F) < 1 := by decide
 #align counterexample.F.z01 Counterexample.F.z01
 
+instance : Add F where
+  add := max
+
 /-- `F` would be a `CommSemiring`, using `min` as multiplication.  Again, we do not need this. -/
 instance : AddCommMonoid F where
-  add := max
   add_assoc := by boom
   zero := 0
   zero_add := by boom
   add_zero := by boom
   add_comm := by boom
+  nsmul := nsmulRec
 
 /-- The `CovariantClass`es asserting monotonicity of addition hold for `F`. -/
 instance covariantClass_add_le : CovariantClass F F (· + ·) (· ≤ ·) :=

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -108,17 +108,25 @@ def ColimitType : Type max u v w :=
   Quotient (colimitSetoid.{w} F)
 #align AddCommGroup.colimits.colimit_type AddCommGroupCat.Colimits.ColimitType
 
-instance : AddCommGroup (ColimitType.{w} F) where
+instance : Zero (ColimitType.{w} F) where
   zero := Quotient.mk _ zero
+
+instance : Neg (ColimitType.{w} F) where
   neg := Quotient.map neg Relation.neg_1
-  add := Quotient.map₂ add fun x x' rx y y' ry =>
+
+instance : Add (ColimitType.{w} F) where
+  add := Quotient.map₂ add <| fun _x x' rx y _y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
-  zero_add := Quotient.ind fun _ => Quotient.sound <| Relation.zero_add _
-  add_zero := Quotient.ind fun _ => Quotient.sound <| Relation.add_zero _
-  add_left_neg := Quotient.ind fun _ => Quotient.sound <| Relation.add_left_neg _
-  add_comm := Quotient.ind₂ fun _ _ => Quotient.sound <| Relation.add_comm _ _
-  add_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
+
+instance : AddCommGroup (ColimitType.{w} F) where
+  zero_add := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_add _
+  add_zero := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_zero _
+  add_left_neg := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_left_neg _
+  add_comm := Quotient.ind₂ <| fun _ _ => Quotient.sound <| Relation.add_comm _ _
+  add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
+  nsmul := nsmulRec
+  zsmul := zsmulRec
 
 instance ColimitTypeInhabited : Inhabited (ColimitType.{w} F) := ⟨0⟩
 

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -169,6 +169,8 @@ instance : AddCommGroup (P ⟶ Q) where
   add_zero := by intros; ext1; simp only [add_app, zero_app, add_zero]
   add_comm := by intros; ext1; simp only [add_app]; apply add_comm
   sub_eq_add_neg := by intros; ext1; simp only [add_app, sub_app, neg_app, sub_eq_add_neg]
+  nsmul := nsmulRec
+  zsmul := zsmulRec
 
 instance : Preadditive (PresheafOfModules R) where
   add_comp := by intros; ext1; simp only [comp_app, add_app, comp_add]

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -140,16 +140,24 @@ def ColimitType : Type v :=
   Quotient (colimitSetoid F)
 #align CommRing.colimits.colimit_type CommRingCat.Colimits.ColimitType
 
+instance ColimitType.instZero : Zero (ColimitType F) where zero := Quotient.mk _ zero
+
+instance ColimitType.instAdd : Add (ColimitType F) where
+  add := Quotient.map₂ add <| fun _x x' rx y _y' ry =>
+    Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
+
+instance ColimitType.instNeg : Neg (ColimitType F) where
+  neg := Quotient.map neg Relation.neg_1
+
 instance ColimitType.AddGroup : AddGroup (ColimitType F) where
-  zero := Quotient.mk _ zero
   neg := Quotient.map neg Relation.neg_1
-  add := Quotient.map₂ add fun x x' rx y y' ry =>
-    Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
-  zero_add := Quotient.ind fun _ => Quotient.sound <| Relation.zero_add _
-  add_zero := Quotient.ind fun _ => Quotient.sound <| Relation.add_zero _
-  add_left_neg := Quotient.ind fun _ => Quotient.sound <| Relation.add_left_neg _
-  add_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
+  zero_add := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_add _
+  add_zero := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_zero _
+  add_left_neg := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_left_neg _
+  add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
+  nsmul := nsmulRec
+  zsmul := zsmulRec
 
 -- Porting note: failed to derive `Inhabited` instance
 instance InhabitedColimitType : Inhabited <| ColimitType F where

Mathlib/Algebra/Group/Defs.lean

@@ -593,8 +593,9 @@ need right away.
 
 /-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`. -/
 class AddMonoid (M : Type u) extends AddSemigroup M, AddZeroClass M where
-  /-- Multiplication by a natural number. -/
-  protected nsmul : ℕ → M → M := nsmulRec
+  /-- Multiplication by a natural number.
+  Set this to `nsmulRec` unless `Module` diamonds are possible. -/
+  protected nsmul : ℕ → M → M
   /-- Multiplication by `(0 : ℕ)` gives `0`. -/
   protected nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
   /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
@@ -919,12 +920,15 @@ explanations on this.
 class SubNegMonoid (G : Type u) extends AddMonoid G, Neg G, Sub G where
   protected sub := SubNegMonoid.sub'
   protected sub_eq_add_neg : ∀ a b : G, a - b = a + -b := by intros; rfl
-  protected zsmul : ℤ → G → G := zsmulRec
+  /-- Multiplication by an integer.
+  Set this to `zsmulRec` unless `Module` diamonds are possible. -/
+  protected zsmul : ℤ → G → G
   protected zsmul_zero' : ∀ a : G, zsmul 0 a = 0 := by intros; rfl
   protected zsmul_succ' (n : ℕ) (a : G) :
       zsmul (Int.ofNat n.succ) a = a + zsmul (Int.ofNat n) a := by
     intros; rfl
-  protected zsmul_neg' (n : ℕ) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a := by intros; rfl
+  protected zsmul_neg' (n : ℕ) (a : G) : zsmul (Int.negSucc n) a = -zsmul n.succ a := by
+    intros; rfl
 #align sub_neg_monoid SubNegMonoid
 
 attribute [to_additive SubNegMonoid] DivInvMonoid

Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean

@@ -52,6 +52,8 @@ instance : AddCommGroup (S₁ ⟶ S₂) where
   add_left_neg := fun a => by ext <;> apply add_left_neg
   add_comm := fun a b => by ext <;> apply add_comm
   sub_eq_add_neg := fun a b => by ext <;> apply sub_eq_add_neg
+  nsmul := nsmulRec
+  zsmul := zsmulRec
 
 @[simp] lemma add_τ₁ (φ φ' : S₁ ⟶ S₂) : (φ + φ').τ₁ = φ.τ₁ + φ'.τ₁ := rfl
 @[simp] lemma add_τ₂ (φ φ' : S₁ ⟶ S₂) : (φ + φ').τ₂ = φ.τ₂ + φ'.τ₂ := rfl

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -525,14 +525,16 @@ instance completeLattice : CompleteLattice (LieSubalgebra R L) :=
     inf_le_left := fun _ _ _ ↦ And.left
     inf_le_right := fun _ _ _ ↦ And.right }
 
-instance addCommMonoid : AddCommMonoid (LieSubalgebra R L)
-    where
-  add := (· ⊔ ·)
+instance : Add (LieSubalgebra R L) where add := Sup.sup
+
+instance : Zero (LieSubalgebra R L) where zero := ⊥
+
+instance addCommMonoid : AddCommMonoid (LieSubalgebra R L) where
   add_assoc := sup_assoc
-  zero := ⊥
   zero_add := bot_sup_eq
   add_zero := sup_bot_eq
   add_comm := sup_comm
+  nsmul := nsmulRec
 
 instance : CanonicallyOrderedAddCommMonoid (LieSubalgebra R L) :=
   { LieSubalgebra.addCommMonoid,

Mathlib/Algebra/Lie/Submodule.lean

@@ -556,13 +556,16 @@ theorem iSup_eq_top_iff_coe_toSubmodule {ι : Type*} {N : ι → LieSubmodule R
     ⨆ i, N i = ⊤ ↔ ⨆ i, (N i : Submodule R M) = ⊤ := by
   rw [← iSup_coe_toSubmodule, ← top_coeSubmodule (L := L), coe_toSubmodule_eq_iff]
 
+instance : Add (LieSubmodule R L M) where add := Sup.sup
+
+instance : Zero (LieSubmodule R L M) where zero := ⊥
+
 instance : AddCommMonoid (LieSubmodule R L M) where
-  add := (· ⊔ ·)
   add_assoc := sup_assoc
-  zero := ⊥
   zero_add := bot_sup_eq
   add_zero := sup_bot_eq
   add_comm := sup_comm
+  nsmul := nsmulRec
 
 @[simp]
 theorem add_eq_sup : N + N' = N ⊔ N' :=

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -220,12 +220,14 @@ instance : AddCommMonoid (LocalizedModule S M) where
   nsmul_succ := nsmul_succ'
   add_comm := add_comm'
 
+instance {M : Type*} [AddCommGroup M] [Module R M] : Neg (LocalizedModule S M) where
+  neg p :=
+    liftOn p (fun x => LocalizedModule.mk (-x.1) x.2) fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩ => by
+      rw [mk_eq]
+      exact ⟨u, by simpa⟩
+
 instance {M : Type*} [AddCommGroup M] [Module R M] : AddCommGroup (LocalizedModule S M) :=
   { show AddCommMonoid (LocalizedModule S M) by infer_instance with
-    neg := fun p =>
-      liftOn p (fun x => LocalizedModule.mk (-x.1) x.2) fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩ => by
-        rw [mk_eq]
-        exact ⟨u, by simpa⟩
     add_left_neg := by
       rintro ⟨m, s⟩
       change
@@ -235,7 +237,9 @@ instance {M : Type*} [AddCommGroup M] [Module R M] : AddCommGroup (LocalizedModu
             mk m s =
           0
       rw [liftOn_mk, mk_add_mk]
-      simp }
+      simp
+    -- TODO: fix the diamond
+    zsmul := zsmulRec }
 
 theorem mk_neg {M : Type*} [AddCommGroup M] [Module R M] {m : M} {s : S} : mk (-m) s = -mk m s :=
   rfl

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -164,14 +164,18 @@ end Neg
 
 variable [Semiring R] [AddCommMonoid M] [Module R M]
 
-instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M)
-    where
+instance pointwiseZero : Zero (Submodule R M) where
+  zero := ⊥
+
+instance pointwiseAdd : Add (Submodule R M) where
   add := (· ⊔ ·)
+
+instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M) where
   add_assoc := sup_assoc
-  zero := ⊥
   zero_add := bot_sup_eq
   add_zero := sup_bot_eq
   add_comm := sup_comm
+  nsmul := nsmulRec
 #align submodule.pointwise_add_comm_monoid Submodule.pointwiseAddCommMonoid
 
 @[simp]

Mathlib/Algebra/Order/Group/WithTop.lean

@@ -20,11 +20,13 @@ section LinearOrderedAddCommGroup
 
 variable [LinearOrderedAddCommGroup α] {a b c d : α}
 
+instance instNeg : Neg (WithTop α) where neg := Option.map fun a : α => -a
+
 instance linearOrderedAddCommGroupWithTop : LinearOrderedAddCommGroupWithTop (WithTop α) where
   __ := WithTop.linearOrderedAddCommMonoidWithTop
   __ := Option.nontrivial
-  neg := Option.map fun a : α => -a
   neg_top := Option.map_none
+  zsmul := zsmulRec
   add_neg_cancel := by
     rintro (a | a) ha
     · exact (ha rfl).elim

Mathlib/Algebra/Order/Interval.lean

@@ -541,7 +541,9 @@ instance subtractionCommMonoid {α : Type u} [OrderedAddCommGroup α] :
       exact neg_add_rev _ _
     neg_eq_of_add := fun s t h => by
       obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
-      rw [neg_pure, neg_eq_of_add_eq_zero_right hab] }
+      rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
+    -- TODO: use a better defeq
+    zsmul := zsmulRec }
 
 @[to_additive existing NonemptyInterval.subtractionCommMonoid]
 instance divisionCommMonoid : DivisionCommMonoid (NonemptyInterval α) :=
@@ -590,7 +592,9 @@ instance subtractionCommMonoid {α : Type u} [OrderedAddCommGroup α] :
       rintro (_ | s) (_ | t) h <;>
         first
           | cases h
-          | exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h) }
+          | exact congr_arg some (neg_eq_of_add_eq_zero_right <| Option.some_injective _ h)
+    -- TODO: use a better defeq
+    zsmul := zsmulRec }
 
 @[to_additive existing Interval.subtractionCommMonoid]
 instance divisionCommMonoid : DivisionCommMonoid (Interval α) :=

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -452,6 +452,8 @@ def GeneralizedBooleanAlgebra.toNonUnitalCommRing [GeneralizedBooleanAlgebra α]
   mul_comm := inf_comm
   left_distrib := inf_symmDiff_distrib_left
   right_distrib := inf_symmDiff_distrib_right
+  nsmul := letI : Zero α := ⟨⊥⟩; letI : Add α := ⟨(· ∆ ·)⟩; nsmulRec
+  zsmul := letI : Zero α := ⟨⊥⟩; letI : Add α := ⟨(· ∆ ·)⟩; letI : Neg α := ⟨id⟩; zsmulRec
 #align generalized_boolean_algebra.to_non_unital_comm_ring GeneralizedBooleanAlgebra.toNonUnitalCommRing
 
 instance [GeneralizedBooleanAlgebra α] : NonUnitalCommRing (AsBoolRing α) :=
@@ -588,19 +590,25 @@ def RingEquiv.asBoolRingAsBoolAlg (α : Type*) [BooleanRing α] : AsBoolRing (As
 
 open Bool
 
+instance : Zero Bool where zero := false
+
+instance : One Bool where one := true
+
+instance : Add Bool where add := xor
+
+instance : Neg Bool where neg := id
+
+instance : Sub Bool where sub := xor
+
+instance : Mul Bool where mul := and
+
 instance : BooleanRing Bool where
-  add := xor
   add_assoc := xor_assoc
-  zero := false
   zero_add := Bool.false_xor
   add_zero := Bool.xor_false
-  neg := id
-  sub := xor
   sub_eq_add_neg _ _ := rfl
   add_left_neg := Bool.xor_self
   add_comm := xor_comm
-  one := true
-  mul := and
   mul_assoc := and_assoc
   one_mul := Bool.true_and
   mul_one := Bool.and_true
@@ -609,3 +617,5 @@ instance : BooleanRing Bool where
   mul_self := Bool.and_self
   zero_mul a := rfl
   mul_zero a := by cases a <;> rfl
+  nsmul := nsmulRec
+  zsmul := zsmulRec

Mathlib/Algebra/Ring/MinimalAxioms.lean

@@ -67,7 +67,8 @@ def Ring.ofMinimalAxioms {R : Type u}
     mul_assoc := mul_assoc
     one_mul := one_mul
     mul_one := mul_one
-    add_left_neg := add_left_neg }
+    add_left_neg := add_left_neg
+    zsmul := (· • ·) }
 
 /-- Define a `CommRing` structure on a Type by proving a minimized set of axioms.
 Note that this uses the default definitions for `npow`, `nsmul`, `zsmul` and `sub`

Mathlib/Algebra/Tropical/Basic.lean

@@ -373,7 +373,8 @@ theorem add_eq_zero_iff {a b : Tropical (WithTop R)} : a + b = 0 ↔ a = 0 ∧ b
 instance instAddCommMonoidTropical [OrderTop R] : AddCommMonoid (Tropical R) :=
   { instZeroTropical, instAddCommSemigroupTropical with
     zero_add := fun _ => untrop_injective (min_top_left _)
-    add_zero := fun _ => untrop_injective (min_top_right _) }
+    add_zero := fun _ => untrop_injective (min_top_right _)
+    nsmul := nsmulRec }
 
 end Order
 

Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean

@@ -631,6 +631,8 @@ lemma add_assoc (P Q R : W.Point) : P + Q + R = P + (Q + R) :=
 #align weierstrass_curve.point.add_assoc WeierstrassCurve.Affine.Point.add_assoc
 
 noncomputable instance instAddCommGroupPoint : AddCommGroup W.Point where
+  nsmul := nsmulRec
+  zsmul := zsmulRec
   zero_add := zero_add
   add_zero := add_zero
   add_left_neg := add_left_neg

Mathlib/CategoryTheory/Abelian/NonPreadditive.lean

@@ -451,7 +451,9 @@ def preadditive : Preadditive C where
       neg := fun f => -f
       add_left_neg := neg_add_self
       sub_eq_add_neg := fun f g => (add_neg f g).symm -- Porting note: autoParam failed
-      add_comm := add_comm }
+      add_comm := add_comm
+      nsmul := nsmulRec
+      zsmul := zsmulRec }
   add_comp := add_comp
   comp_add := comp_add
 #align category_theory.non_preadditive_abelian.preadditive CategoryTheory.NonPreadditiveAbelian.preadditive

Mathlib/CategoryTheory/Idempotents/Biproducts.lean

@@ -108,15 +108,15 @@ instance (P : Karoubi C) : HasBinaryBiproduct P P.complement :=
       inr := P.complement.decompId_i
       inl_fst := P.decompId.symm
       inl_snd := by
-        simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f,
+        simp only [instZero_zero, hom_ext_iff, complement_X, comp_f,
           decompId_i_f, decompId_p_f, complement_p, comp_sub, comp_id, idem, sub_self]
       inr_fst := by
-        simp only [instAddCommGroupHom_zero, hom_ext_iff, complement_X, comp_f,
+        simp only [instZero_zero, hom_ext_iff, complement_X, comp_f,
           decompId_i_f, complement_p, decompId_p_f, sub_comp, id_comp, idem, sub_self]
       inr_snd := P.complement.decompId.symm }
     (by
       simp only [id_eq, complement_X, comp_f,
-        decompId_i_f, decompId_p_f, complement_p, instAddCommGroupHom_add, idem,
+        decompId_i_f, decompId_p_f, complement_p, instAdd_add, idem,
         comp_sub, comp_id, sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel'_right])
 
 attribute [-simp] hom_ext_iff
@@ -134,15 +134,15 @@ def decomposition (P : Karoubi C) : P ⊞ P.complement ≅ (toKaroubi _).obj P.X
       refine' (_ =≫ _).trans zero_comp
       ext
       simp only [comp_f, toKaroubi_obj_X, decompId_i_f, decompId_p_f,
-        complement_p, comp_sub, comp_id, idem, sub_self, instAddCommGroupHom_zero]
+        complement_p, comp_sub, comp_id, idem, sub_self, instZero_zero]
     · rw [biprod.inr_desc_assoc, comp_id, biprod.lift_eq, comp_add, ← decompId_assoc,
         add_left_eq_self, ← assoc]
       refine' (_ =≫ _).trans zero_comp
       ext
       simp only [complement_X, comp_f, decompId_i_f, complement_p,
-        decompId_p_f, sub_comp, id_comp, idem, sub_self, instAddCommGroupHom_zero]
+        decompId_p_f, sub_comp, id_comp, idem, sub_self, instZero_zero]
   inv_hom_id := by
-    simp only [biprod.lift_desc, instAddCommGroupHom_add, toKaroubi_obj_X, comp_f,
+    simp only [biprod.lift_desc, instAdd_add, toKaroubi_obj_X, comp_f,
       decompId_p_f, decompId_i_f, idem, complement_X, complement_p, comp_sub, comp_id,
       sub_comp, id_comp, sub_self, sub_zero, add_sub_cancel'_right,
       id_eq, toKaroubi_obj_p]