refactor: do not allow qsmul to default automatically (#11262)

Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
leanprover-community · Apr 15, 2024 · b709282 · b709282
1 parent c30e6d5
commit b709282
Show file tree

Hide file tree

Showing 22 changed files with 45 additions and 24 deletions.
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
@@ -1027,7 +1027,8 @@ protected noncomputable def field [DirectedSystem G fun i j h => f' i j h] :
   -- but leaving them implicit avoids a very expensive (2-3 minutes!) eta expansion.
   { inv := inv G fun i j h => f' i j h
     mul_inv_cancel := fun p => DirectLimit.mul_inv_cancel G fun i j h => f' i j h
-    inv_zero := dif_pos rfl }
+    inv_zero := dif_pos rfl
+    qsmul := qsmulRec _ }
 #align field.direct_limit.field Field.DirectLimit.field
 
 end

diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean
@@ -267,15 +267,15 @@ variable {R : Type*} [Nontrivial R]
 /-- Constructs a `DivisionRing` structure on a `Ring` consisting only of units and 0. -/
 noncomputable def divisionRingOfIsUnitOrEqZero [hR : Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
     DivisionRing R :=
-  { groupWithZeroOfIsUnitOrEqZero h, hR with }
+  { groupWithZeroOfIsUnitOrEqZero h, hR with qsmul := qsmulRec _}
 #align division_ring_of_is_unit_or_eq_zero divisionRingOfIsUnitOrEqZero
 
 /-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0.
 See note [reducible non-instances]. -/
 @[reducible]
 noncomputable def fieldOfIsUnitOrEqZero [hR : CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
     Field R :=
-  { groupWithZeroOfIsUnitOrEqZero h, hR with }
+  { divisionRingOfIsUnitOrEqZero h, hR with }
 #align field_of_is_unit_or_eq_zero fieldOfIsUnitOrEqZero
 
 end NoncomputableDefs

diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean
@@ -94,8 +94,9 @@ class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, Ra
   protected ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 h2), Rat.cast ⟨a, b, h1, h2⟩ = a * (b : K)⁻¹ := by
     intros
     rfl
-  /-- Multiplication by a rational number. -/
-  protected qsmul : ℚ → K → K := qsmulRec Rat.cast
+  /-- Multiplication by a rational number.
+  Set this to `qsmulRec _` unless there is a risk of a `Module ℚ _` instance diamond. -/
+  protected qsmul : ℚ → K → K
   /-- However `qsmul` is defined,
   propositionally it must be equal to multiplication by `ratCast`. -/
   protected qsmul_eq_mul' : ∀ (a : ℚ) (x : K), qsmul a x = Rat.cast a * x := by

diff --git a/Mathlib/Algebra/Field/IsField.lean b/Mathlib/Algebra/Field/IsField.lean
@@ -74,7 +74,7 @@ noncomputable def IsField.toSemifield {R : Type u} [Semiring R] (h : IsField R)
 
 /-- Transferring from `IsField` to `Field`. -/
 noncomputable def IsField.toField {R : Type u} [Ring R] (h : IsField R) : Field R :=
-  { ‹Ring R›, IsField.toSemifield h with }
+  { ‹Ring R›, IsField.toSemifield h with qsmul := qsmulRec _ }
 #align is_field.to_field IsField.toField
 
 /-- For each field, and for each nonzero element of said field, there is a unique inverse.

diff --git a/Mathlib/Algebra/Field/MinimalAxioms.lean b/Mathlib/Algebra/Field/MinimalAxioms.lean
@@ -41,4 +41,5 @@ def Field.ofMinimalAxioms (K : Type u)
     add_left_neg mul_assoc mul_comm one_mul left_distrib
   { exists_pair_ne := exists_pair_ne
     mul_inv_cancel := mul_inv_cancel
-    inv_zero := inv_zero }
+    inv_zero := inv_zero
+    qsmul := qsmulRec _ }
diff --git a/Mathlib/Algebra/Field/Opposite.lean b/Mathlib/Algebra/Field/Opposite.lean
@@ -46,7 +46,8 @@ instance divisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ :=
   { MulOpposite.divisionSemiring α, MulOpposite.ring α, MulOpposite.ratCast α with
     ratCast_mk := fun a b hb h => unop_injective <| by
       rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
-        Int.commute_cast, div_eq_mul_inv] }
+        Int.commute_cast, div_eq_mul_inv]
+    qsmul := qsmulRec _ }
 
 instance semifield [Semifield α] : Semifield αᵐᵒᵖ :=
   { MulOpposite.divisionSemiring α, MulOpposite.commSemiring α with }
@@ -65,7 +66,8 @@ instance divisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ :=
   { AddOpposite.ring α, AddOpposite.groupWithZero α, AddOpposite.ratCast α with
     ratCast_mk := fun a b hb h => unop_injective <| by
       rw [unop_ratCast, Rat.cast_def, unop_mul, unop_inv, unop_natCast, unop_intCast,
-        div_eq_mul_inv] }
+        div_eq_mul_inv]
+    qsmul := qsmulRec _ }
 
 instance semifield [Semifield α] : Semifield αᵃᵒᵖ :=
   { AddOpposite.divisionSemiring, AddOpposite.commSemiring α with }

diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean
@@ -276,6 +276,7 @@ noncomputable instance Cauchy.divisionRing : DivisionRing (Cauchy abv) where
   mul_inv_cancel x := CauSeq.Completion.mul_inv_cancel
   ratCast q := ofRat q
   ratCast_mk n d hd hnd := by rw [← ofRat_ratCast, Rat.cast_mk', ofRat_mul, ofRat_inv]; rfl
+  qsmul := qsmulRec _ -- TODO: fix instance diamond
 
 theorem ofRat_div (x y : β) : ofRat (x / y) = (ofRat x / ofRat y : Cauchy abv) := by
   simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul]

diff --git a/Mathlib/CategoryTheory/Preadditive/Schur.lean b/Mathlib/CategoryTheory/Preadditive/Schur.lean
@@ -76,7 +76,8 @@ noncomputable instance [HasKernels C] {X : C} [Simple X] : DivisionRing (End X)
         dsimp
         rw [dif_neg h]
         haveI := isIso_of_hom_simple h
-        exact IsIso.inv_hom_id f }
+        exact IsIso.inv_hom_id f
+      qsmul := qsmulRec _ }
 
 open FiniteDimensional
 

diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean
@@ -586,7 +586,8 @@ noncomputable instance : LinearOrderedField ℝ :=
     ratCast := (↑)
     ratCast_mk := fun n d hd h2 => by
       rw [← ofCauchy_ratCast, Rat.cast_mk', ofCauchy_mul, ofCauchy_inv, ofCauchy_natCast,
-        ofCauchy_intCast] }
+        ofCauchy_intCast]
+    qsmul := qsmulRec _ }
 
 -- Extra instances to short-circuit type class resolution
 noncomputable instance : LinearOrderedAddCommGroup ℝ := by infer_instance

diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
@@ -1248,7 +1248,8 @@ instance : Field (ZMod p) :=
   { inferInstanceAs (CommRing (ZMod p)), inferInstanceAs (Inv (ZMod p)),
     ZMod.nontrivial p with
     mul_inv_cancel := mul_inv_cancel_aux p
-    inv_zero := inv_zero p }
+    inv_zero := inv_zero p
+    qsmul := qsmulRec _ }
 
 /-- `ZMod p` is an integral domain when `p` is prime. -/
 instance (p : ℕ) [hp : Fact p.Prime] : IsDomain (ZMod p) := by

diff --git a/Mathlib/FieldTheory/PerfectClosure.lean b/Mathlib/FieldTheory/PerfectClosure.lean
@@ -510,7 +510,8 @@ instance instDivisionRing : DivisionRing (PerfectClosure K p) :=
         simp only [(frobenius _ _).iterate_map_one, (frobenius K p).iterate_map_zero,
             iterate_zero_apply, ← iterate_map_mul] at this ⊢
         rw [mul_inv_cancel this, (frobenius _ _).iterate_map_one]
-    inv_zero := congr_arg (Quot.mk (R K p)) (by rw [inv_zero]) }
+    inv_zero := congr_arg (Quot.mk (R K p)) (by rw [inv_zero])
+    qsmul := qsmulRec _ }
 
 instance instField : Field (PerfectClosure K p) :=
   { (inferInstance : DivisionRing (PerfectClosure K p)),

diff --git a/Mathlib/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean
@@ -791,7 +791,8 @@ instance instField [IsDomain K] : Field (RatFunc K) :=
     div := (· / ·)
     div_eq_mul_inv := by frac_tac
     mul_inv_cancel := fun _ => mul_inv_cancel
-    zpow := zpowRec }
+    zpow := zpowRec
+    qsmul := qsmulRec _ }
 
 section IsFractionRing
 

diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -856,7 +856,8 @@ noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [h : R
       show x * dite _ (h := _) _ = _ by
         rw [dif_neg hx]
         exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
-    inv_zero := dif_pos rfl }
+    inv_zero := dif_pos rfl
+    qsmul := qsmulRec _ }
 #align division_ring_of_finite_dimensional divisionRingOfFiniteDimensional
 
 /-- An integral domain that is module-finite as an algebra over a field is a field. -/

diff --git a/Mathlib/Order/Filter/FilterProduct.lean b/Mathlib/Order/Filter/FilterProduct.lean
@@ -51,7 +51,7 @@ instance divisionSemiring [DivisionSemiring β] : DivisionSemiring β* where
   __ := Germ.groupWithZero
 
 instance divisionRing [DivisionRing β] : DivisionRing β* :=
-  { Germ.ring, Germ.divisionSemiring with }
+  { Germ.ring, Germ.divisionSemiring with qsmul := qsmulRec _ }
 
 instance semifield [Semifield β] : Semifield β* :=
   { Germ.commSemiring, Germ.divisionSemiring with }

diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean
@@ -591,7 +591,8 @@ instance [Field R] : Field (HahnSeries Γ R) :=
         SummableFamily.one_sub_self_mul_hsum_powers
           (unit_aux x (inv_mul_cancel (coeff_order_ne_zero x0)))
       rw [sub_sub_cancel] at h
-      rw [← mul_assoc, mul_comm x, h] }
+      rw [← mul_assoc, mul_comm x, h]
+    qsmul := qsmulRec _ }
 
 end Inversion
 

diff --git a/Mathlib/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient.lean
@@ -225,7 +225,7 @@ will have computable inverses (and `qsmul`, `rat_cast`) in some applications.
 See note [reducible non-instances]. -/
 @[reducible]
 protected noncomputable def field (I : Ideal R) [hI : I.IsMaximal] : Field (R ⧸ I) :=
-  { Quotient.commRing I, Quotient.groupWithZero I with }
+  { Quotient.commRing I, Quotient.groupWithZero I with qsmul := qsmulRec _ }
 #align ideal.quotient.field Ideal.Quotient.field
 
 /-- If the quotient by an ideal is a field, then the ideal is maximal. -/

diff --git a/Mathlib/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean
@@ -96,13 +96,14 @@ variable [Ring R] [IsDomain R] [Fintype R]
 `Mathlib.RingTheory.LittleWedderburn`. -/
 def Fintype.divisionRingOfIsDomain (R : Type*) [Ring R] [IsDomain R] [DecidableEq R] [Fintype R] :
     DivisionRing R :=
-  { show GroupWithZero R from Fintype.groupWithZeroOfCancel R, ‹Ring R› with }
+  { show GroupWithZero R from Fintype.groupWithZeroOfCancel R, ‹Ring R› with
+    qsmul := qsmulRec _}
 #align fintype.division_ring_of_is_domain Fintype.divisionRingOfIsDomain
 
 /-- Every finite commutative domain is a field. More generally, commutativity is not required: this
 can be found in `Mathlib.RingTheory.LittleWedderburn`. -/
 def Fintype.fieldOfDomain (R) [CommRing R] [IsDomain R] [DecidableEq R] [Fintype R] : Field R :=
-  { Fintype.groupWithZeroOfCancel R, ‹CommRing R› with }
+  { Fintype.divisionRingOfIsDomain R, ‹CommRing R› with }
 #align fintype.field_of_domain Fintype.fieldOfDomain
 
 theorem Finite.isField_of_domain (R) [CommRing R] [IsDomain R] [Finite R] : IsField R := by

diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -140,7 +140,8 @@ noncomputable def toField : Field K :=
     inv_zero := by
       change IsFractionRing.inv A (0 : K) = 0
       rw [IsFractionRing.inv]
-      exact dif_pos rfl }
+      exact dif_pos rfl
+    qsmul := qsmulRec _ }
 #align is_fraction_ring.to_field IsFractionRing.toField
 
 lemma surjective_iff_isField [IsDomain R] : Function.Surjective (algebraMap R K) ↔ IsField R where

diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -932,7 +932,8 @@ instance divisionRing : DivisionRing R[R⁰⁻¹] :=
     OreLocalization.inv',
     OreLocalization.ring with
     mul_inv_cancel := OreLocalization.mul_inv_cancel
-    inv_zero := OreLocalization.inv_zero }
+    inv_zero := OreLocalization.inv_zero
+    qsmul := qsmulRec _ }
 
 end DivisionRing
 

diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean
@@ -405,6 +405,7 @@ noncomputable instance _root_.Module.End.divisionRing
     simp_rw [dif_neg a0]; ext
     exact (LinearEquiv.ofBijective _ <| bijective_of_ne_zero a0).right_inv _
   inv_zero := dif_pos rfl
+  qsmul := qsmulRec _
 #align module.End.division_ring Module.End.divisionRing
 
 end LinearMap

diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean
@@ -771,7 +771,9 @@ instance : Field (center K) :=
     mul_inv_cancel := fun ⟨a, ha⟩ h => Subtype.ext <| mul_inv_cancel <| Subtype.coe_injective.ne h
     div := fun a b => ⟨a / b, Set.div_mem_center₀ a.prop b.prop⟩
     div_eq_mul_inv := fun a b => Subtype.ext <| div_eq_mul_inv _ _
-    inv_zero := Subtype.ext inv_zero }
+    inv_zero := Subtype.ext inv_zero
+    -- TODO: use a nicer defeq
+    qsmul := qsmulRec _ }
 
 @[simp]
 theorem center.coe_inv (a : center K) : ((a⁻¹ : center K) : K) = (a : K)⁻¹ :=

diff --git a/Mathlib/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean
@@ -160,7 +160,9 @@ instance instField : Field (hat K) :=
     (by infer_instance : CommRing (hat K)) with
     exists_pair_ne := ⟨0, 1, fun h => zero_ne_one ((uniformEmbedding_coe K).inj h)⟩
     mul_inv_cancel := fun x x_ne => by simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]
-    inv_zero := by simp only [Inv.inv, ite_true] }
+    inv_zero := by simp only [Inv.inv, ite_true]
+    -- TODO: use a better defeq
+    qsmul := qsmulRec _ }
 #align uniform_space.completion.field UniformSpace.Completion.instField
 
 instance : TopologicalDivisionRing (hat K) :=