Skip to content

Commit

Permalink
fix: generalize DivisionRing.toOfScientific (#9947)
Browse files Browse the repository at this point in the history
If you can cast a rat to a type, then we probably want decimal notation to work there too.

This has the benefit of making the instance computable even in cases where some parts of the division ring structure are not.
It also means that this could apply to matrices of rational numbers, which are not a division ring, but could have a rat cast.
  • Loading branch information
eric-wieser authored and Vierkantor committed Feb 5, 2024
1 parent 9094856 commit 8405080
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Field/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ end DivisionRing

section OfScientific

instance DivisionRing.toOfScientific [DivisionRing K] : OfScientific K where
instance RatCast.toOfScientific [RatCast K] : OfScientific K where
ofScientific (m : ℕ) (b : Bool) (d : ℕ) := Rat.ofScientific m b d

end OfScientific
Expand Down

0 comments on commit 8405080

Please sign in to comment.