From 1071cb9cd8f1f2e6c4de0dcb46cca26408805b21 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Fri, 22 May 2026 10:07:31 +0100 Subject: [PATCH] build --- Mathlib/Algebra/Group/Units/Hom.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Group/Units/Hom.lean b/Mathlib/Algebra/Group/Units/Hom.lean index 253a16e52bc046..9445d40f862d78 100644 --- a/Mathlib/Algebra/Group/Units/Hom.lean +++ b/Mathlib/Algebra/Group/Units/Hom.lean @@ -267,11 +267,11 @@ variable [Monoid R] [Monoid S] [Monoid T] [FunLike F R S] whenever `f a` is a unit. See `IsLocalRing.local_hom_TFAE` for other equivalent definitions in the local ring case - from where this concept originates, but it is useful in other contexts, so we allow this generalisation in mathlib. -/ -class IsLocalHom (f : F) : Prop where +class IsLocalHom (f : R → S) : Prop where /-- A local homomorphism `f : R ⟶ S` will send nonunits of `R` to nonunits of `S`. -/ map_nonunit : ∀ a, IsUnit (f a) → IsUnit a -theorem IsUnit.of_map (f : F) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a := +theorem IsUnit.of_map (f : R → S) [IsLocalHom f] (a : R) (h : IsUnit (f a)) : IsUnit a := IsLocalHom.map_nonunit a h -- TODO : remove alias, change the parenthesis of `f` and `a`