Skip to content

Commit 10bacfb

Browse files
committed
Lint fix
1 parent 76efd2e commit 10bacfb

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Algebra/Category/Ring/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,6 @@ Authors: Kim Morrison, Johannes Hölzl, Yury Kudryashov
55
-/
66
import Mathlib.Algebra.Category.Grp.Basic
77
import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
8-
import Mathlib.CategoryTheory.Elementwise
98
import Mathlib.Algebra.Ring.Equiv
109

1110
/-!
@@ -380,6 +379,7 @@ instance : ConcreteCategory.{u} CommSemiRingCat (fun R S => R →+* S) where
380379
hom := Hom.hom'
381380
ofHom f := ⟨f⟩
382381

382+
/-- Turn a morphism in `CommSemiRingCat` back into a `RingHom`. -/
383383
abbrev Hom.hom {R S : CommSemiRingCat.{u}} (f : Hom R S) :=
384384
ConcreteCategory.hom (C := CommSemiRingCat) f
385385

0 commit comments

Comments
 (0)