From 1903dbae6f714e3c48a7df3b4c4ca2f185d113ba Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sun, 19 Apr 2026 14:10:39 +0200 Subject: [PATCH] fix --- Mathlib/Algebra/Field/Subfield/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Field/Subfield/Basic.lean b/Mathlib/Algebra/Field/Subfield/Basic.lean index f71d10ed60d7c4..0f34ab90c7b2b1 100644 --- a/Mathlib/Algebra/Field/Subfield/Basic.lean +++ b/Mathlib/Algebra/Field/Subfield/Basic.lean @@ -550,7 +550,7 @@ protected theorem prod_mem {ι : Type*} {t : Finset ι} {f : ι → K} (h : ∀ prod_mem h instance toAlgebra : Algebra s K := - RingHom.toAlgebra s.subtype + fast_instance% RingHom.toAlgebra s.subtype theorem algebraMap_ofSubfield : algebraMap s K = s.subtype := rfl