Skip to content

Commit b5b0f56

Browse files
NoahW314Bergschaf
authored andcommitted
doc(CategoryTheory): fix typo (leanprover-community#39737)
Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>
1 parent 1f8d7a2 commit b5b0f56

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/CategoryTheory/Preadditive/Projective/Resolution.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,7 @@ noncomputable def self [Projective Z] : ProjectiveResolution Z where
137137

138138
variable {Z} {Z' : C} (P' : ProjectiveResolution Z')
139139

140-
/-- Given injective resolutions `P` and `P'` of two objects `Z` and `Z'`,
140+
/-- Given projective resolutions `P` and `P'` of two objects `Z` and `Z'`,
141141
and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
142142
`P.complex ⟶ P'.complex` which is compatible with `f` -/
143143
structure Hom (f : Z ⟶ Z') where

0 commit comments

Comments
 (0)