From 23f4bc017dacb0eb4ef1e70d84c552e3608b91b7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 23 Jan 2024 23:52:16 +0000 Subject: [PATCH] fix: generalize DivisionRing.toOfScientific If you can cast a rat to a type, then we probably want decimal notation to work there too --- 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 6c04525a57ec9..f9605553ee0e3 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