From 840508050b65083c36a84d2514ab210a24cfb768 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 5 Feb 2024 00:24:14 +0000 Subject: [PATCH] fix: generalize DivisionRing.toOfScientific (#9947) 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. --- Mathlib/Algebra/Field/Defs.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean index 6c04525a57ec92..f9605553ee0e35 100644 --- a/Mathlib/Algebra/Field/Defs.lean +++ b/Mathlib/Algebra/Field/Defs.lean @@ -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