Update Mathlib/RingTheory/LocalProperties/Projective.lean

Co-authored-by: Christian Merten <[email protected]>
leanprover-community · Oct 31, 2024 · e35c74a · e35c74a
1 parent 4e810db
commit e35c74a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/LocalProperties/Projective.lean b/Mathlib/RingTheory/LocalProperties/Projective.lean
@@ -14,7 +14,7 @@ import Mathlib.RingTheory.Localization.BaseChange
 # Being projective is a local property
 
 ## Main results
-- `split_surjective_of_localization_maximal` If `N` is finitely presented, then `f : M →ₗ[R] N`
+- `LinearMap.split_surjective_of_localization_maximal` If `N` is finitely presented, then `f : M →ₗ[R] N`
   being split injective can be checked on stalks (of maximal ideals).
 - `Module.projective_of_localization_maximal` If `M` is finitely presented,
   then `M` being projective can be checked on stalks (of maximal ideals).