Skip to content

Commit

Permalink
chore(category_theory/abelian/projective): fix typo (#12701)
Browse files Browse the repository at this point in the history
  • Loading branch information
jjaassoonn committed Mar 15, 2022
1 parent 92e6759 commit 078b213
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/category_theory/abelian/projective.lean
Expand Up @@ -61,7 +61,7 @@ chain_complex.mk'

/--
In any abelian category with enough projectives,
`ProjectiveResolution.of Z` constructs a projection resolution of the object `Z`.
`ProjectiveResolution.of Z` constructs a projective resolution of the object `Z`.
-/
@[irreducible] def of (Z : C) : ProjectiveResolution Z :=
{ complex := of_complex Z,
Expand Down

0 comments on commit 078b213

Please sign in to comment.