From c5c8fe550b76c66410d49a083cb7ecc6af493dc8 Mon Sep 17 00:00:00 2001 From: yhtq <1414672068@qq.com> Date: Wed, 30 Oct 2024 22:38:18 +0800 Subject: [PATCH] Update Mathlib/Algebra/Algebra/Defs.lean Co-authored-by: Eric Wieser --- Mathlib/Algebra/Algebra/Defs.lean | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean index 85a8162100460..794d5d7892ee8 100644 --- a/Mathlib/Algebra/Algebra/Defs.lean +++ b/Mathlib/Algebra/Algebra/Defs.lean @@ -331,13 +331,11 @@ variable {R : Type u} {S : Type v} (A : Type w) /-- Compose a Algebra with a RingHom, with action f s • m. -/ -abbrev compHom: Algebra S A := - { - (algebraMap R A).comp f with - smul := fun s x => f s • x - commutes' := fun _ _ => Algebra.commutes' _ _, - smul_def' := fun s x => smul_def (f s) x - } +abbrev compHom: Algebra S A where + smul s a := f s • a + toRingHom := (algebraMap R A).comp f + commutes' _ _ := Algebra.commutes _ _ + smul_def' _ _ := Algebra.smul_def _ _ theorem compHom_smul_def (s : S) (x : A): letI := compHom A f