-
Notifications
You must be signed in to change notification settings - Fork 259
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor: do not allow qsmul
to default automatically
#11262
Conversation
!bench |
@@ -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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe make a separate issue or add to an existing one.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Easier to just fix it, #11263
Here are the benchmark results for commit cb4d250. Benchmark Metric Change
==========================================================
+ build linting -5.6%
+ ~Mathlib.RingTheory.IntegralDomain instructions -39.7% |
#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 } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess this caused the speedup?
bors merge |
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Is that PR the start of the doom of Type-valued default fields? |
For now I think it's only the ones involved in diamonds that matter. There'd be no benefit to changing |
|
Pull request successfully merged into master. Build succeeded: |
qsmul
to default automaticallyqsmul
to default automatically
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262. Again, this does not attempt to fix any diamonds; it only identifies where they may be.
Follows on from #6262.
Again, this does not attempt to fix any diamonds; it only identifies where they may be.