From 034d64df09566c28e83315865bb724858a983ae6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 12:10:45 +0000 Subject: [PATCH 1/7] refactor: do not allow `qsmul` to default automatically --- Mathlib/Algebra/Field/Basic.lean | 4 ++-- Mathlib/Algebra/Field/Defs.lean | 5 +++-- Mathlib/Algebra/Field/IsField.lean | 2 +- Mathlib/Algebra/Field/MinimalAxioms.lean | 3 ++- Mathlib/Algebra/Field/Opposite.lean | 6 ++++-- Mathlib/Algebra/Order/CauSeq/Completion.lean | 1 + Mathlib/Order/Filter/FilterProduct.lean | 2 +- Mathlib/RingTheory/OreLocalization/Basic.lean | 3 ++- Mathlib/RingTheory/Subring/Basic.lean | 4 +++- 9 files changed, 19 insertions(+), 11 deletions(-) diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean index 94a8f28485fd1..8c36b8dc4a9c6 100644 --- a/Mathlib/Algebra/Field/Basic.lean +++ b/Mathlib/Algebra/Field/Basic.lean @@ -267,7 +267,7 @@ 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. @@ -275,7 +275,7 @@ 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 index f9605553ee0e3..653773481e641 100644 --- 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 index 8868b485f87ad..016668a094f15 100644 --- 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 index 8358b234582d4..360b33f28883e 100644 --- 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 index f316f3e7da0f4..8d5da6e4cfa5b 100644 --- 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 index 53cc5d09563e5..033bba44ace90 100644 --- 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/Order/Filter/FilterProduct.lean b/Mathlib/Order/Filter/FilterProduct.lean index d84c29cbc086f..c6abf1cc21fce 100644 --- 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/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean index f1a59d6bb4963..35720d334f202 100644 --- 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/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean index c1b992d70a04d..3e7c04225a8d6 100644 --- 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)⁻¹ := From c64c281ecfd2a623b3c434e9e61e8986c73309e2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 12:18:49 +0000 Subject: [PATCH 2/7] fix --- Mathlib/Data/Real/Basic.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Data/Real/Basic.lean b/Mathlib/Data/Real/Basic.lean index 155b008f6e9f3..2eb42d282f831 100644 --- 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 From 2c87a683cb2db2df609969f1d62d54bbaeb38b72 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 12:38:33 +0000 Subject: [PATCH 3/7] two more --- Mathlib/RingTheory/HahnSeries/Summable.lean | 3 ++- Mathlib/RingTheory/Localization/FractionRing.lean | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/HahnSeries/Summable.lean b/Mathlib/RingTheory/HahnSeries/Summable.lean index a438da982e0cc..50b9f425f01d5 100644 --- 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/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index c67dfc1bddb55..ddc85cea1ee84 100644 --- 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 From 7c3e4fb8bfa46b9128fe927d5fb2e74f445c5ed9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 12:40:32 +0000 Subject: [PATCH 4/7] two more --- Mathlib/Data/ZMod/Basic.lean | 3 ++- Mathlib/RingTheory/Ideal/Quotient.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean index 748efae8b05d7..e03c2fed79f66 100644 --- 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/RingTheory/Ideal/Quotient.lean b/Mathlib/RingTheory/Ideal/Quotient.lean index 436ea435275ad..c0cb28ef4dd53 100644 --- 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. -/ From 7f787b4586249fde0c0120a0103ba62ebfd2b2ae Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 13:04:29 +0000 Subject: [PATCH 5/7] more fixes --- Mathlib/Algebra/DirectLimit.lean | 3 ++- Mathlib/FieldTheory/RatFunc.lean | 3 ++- Mathlib/LinearAlgebra/FiniteDimensional.lean | 3 ++- Mathlib/RingTheory/IntegralDomain.lean | 5 +++-- Mathlib/Topology/Algebra/UniformField.lean | 4 +++- 5 files changed, 12 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean index f9874249830bf..7d17727f0d9bd 100644 --- 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/FieldTheory/RatFunc.lean b/Mathlib/FieldTheory/RatFunc.lean index 29cb041ee19aa..17412818d3329 100644 --- 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 index 4475dec033ec8..13047c1c1afab 100644 --- 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/RingTheory/IntegralDomain.lean b/Mathlib/RingTheory/IntegralDomain.lean index f04c1eb1cee82..cb062a038c62a 100644 --- 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/Topology/Algebra/UniformField.lean b/Mathlib/Topology/Algebra/UniformField.lean index 4f78092ed4a3e..a70d4b1f06462 100644 --- 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) := From 0ee17f3f75bcc3c87fa0cc03a43d5b05fd29e2b8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 13:18:28 +0000 Subject: [PATCH 6/7] fix --- Mathlib/RingTheory/SimpleModule.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/RingTheory/SimpleModule.lean b/Mathlib/RingTheory/SimpleModule.lean index 9c319c3f565eb..34860b597510d 100644 --- 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 From cb4d250d59b5487a9537879c219dd454138eed95 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 9 Mar 2024 13:20:10 +0000 Subject: [PATCH 7/7] more --- Mathlib/CategoryTheory/Preadditive/Schur.lean | 3 ++- Mathlib/FieldTheory/PerfectClosure.lean | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Preadditive/Schur.lean b/Mathlib/CategoryTheory/Preadditive/Schur.lean index ffb59c0d50e72..2e3af94ac1c5b 100644 --- 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/FieldTheory/PerfectClosure.lean b/Mathlib/FieldTheory/PerfectClosure.lean index 46eab74a25e60..f4689d0f06d8d 100644 --- 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)),