From 64837c431305e4300a762db1291ef2e764e728fc Mon Sep 17 00:00:00 2001 From: sgouezel Date: Mon, 20 Apr 2026 22:55:06 +0200 Subject: [PATCH] try --- Mathlib/Algebra/Ring/Hom/Defs.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Ring/Hom/Defs.lean b/Mathlib/Algebra/Ring/Hom/Defs.lean index a3f0f3bdb9d5ad..66e0e24fbf223c 100644 --- a/Mathlib/Algebra/Ring/Hom/Defs.lean +++ b/Mathlib/Algebra/Ring/Hom/Defs.lean @@ -534,8 +534,10 @@ theorem coe_monoidHom_id : (id α : α →* α) = MonoidHom.id α := variable {_ : NonAssocSemiring γ} /-- Composition of ring homomorphisms is a ring homomorphism. -/ +@[implicit_reducible] def comp (g : β →+* γ) (f : α →+* β) : α →+* γ := - { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with toFun := g ∘ f, map_one' := by simp } + { g.toNonUnitalRingHom.comp f.toNonUnitalRingHom with + toFun := fun x ↦ g (f x), map_one' := by simp } /-- Composition of semiring homomorphisms is associative. -/ theorem comp_assoc {δ} {_ : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ) :