From eb85ab079381cb0b707624d8c31e0b861cdd8aa8 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 25 Apr 2026 10:35:28 +0200 Subject: [PATCH 1/2] try --- Mathlib/Algebra/Ring/Hom/Defs.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index a3f0f3bdb9d5ad..d636309455dc5f 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -506,6 +506,7 @@ def mk' [NonAssocSemiring α] [NonAssocRing β] (f : α →* β) variable {_ : NonAssocSemiring α} {_ : NonAssocSemiring β} /-- The identity ring homomorphism from a semiring to itself. -/ +@[implicit_reducible] def id (α : Type*) [NonAssocSemiring α] : α →+* α where toFun := _root_.id map_zero' := rfl From dd7df5e064ff3e16f7396f09351c7ec548229bdf Mon Sep 17 00:00:00 2001 From: sgouezel Date: Sat, 25 Apr 2026 14:33:57 +0200 Subject: [PATCH 2/2] drop hack --- Mathlib/Algebra/Algebra/Defs.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean index 3baf9f1f0a2552..d847d42b94ed89 100644 --- a/Mathlib/Algebra/Algebra/Defs.lean +++ b/Mathlib/Algebra/Algebra/Defs.lean @@ -382,11 +382,8 @@ theorem coe_linearMap : ⇑(Algebra.linearMap R A) = algebraMap R A := /-- The identity map inducing an `Algebra` structure. -/ instance (priority := 1100) id : Algebra R R where - -- We override `toFun` and `toSMul` because `RingHom.id` is not reducible and cannot - -- be made so without a significant performance hit. - -- see library note [reducible non-instances]. toSMul := instSMulOfMul - __ := ({ RingHom.id R with toFun x := x }).toAlgebra + __ := (RingHom.id R).toAlgebra @[simp] lemma linearMap_self : Algebra.linearMap R R = .id := rfl