We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 23e5527 commit 367132cCopy full SHA for 367132c
Mathlib/CategoryTheory/Center/Localization.lean
@@ -12,7 +12,7 @@ import Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
12
13
Given a localization functor `L : C ⥤ D` with respect to `W : MorphismProperty C`,
14
we define a localization map `CatCenter C → CatCenter D` for the centers
15
-of these categories. In case `L` is an additive functors between preadditive
+of these categories. In case `L` is an additive functor between preadditive
16
categories, we promote this to a ring morphism `CatCenter C →+* CatCenter D`.
17
18
-/
0 commit comments