doc: fix grammar (#12272)

Change "splitted" to "split".
leanprover-community · Apr 20, 2024 · 8b0bd59 · 8b0bd59
1 parent cccfb03
commit 8b0bd59
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Category/GroupCat/EnoughInjectives.lean b/Mathlib/Algebra/Category/GroupCat/EnoughInjectives.lean
@@ -17,7 +17,7 @@ injective presentation for `A`, hence category of abelian groups has enough inje
 
 ## Implementation notes
 
-This file is splitted from `Mathlib.Algebra.GroupCat.Injective` is to prevent import loop.
+This file is split from `Mathlib.Algebra.GroupCat.Injective` is to prevent import loop.
 This file's dependency imports `Mathlib.Algebra.GroupCat.Injective`.
 -/
 

diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean
@@ -534,7 +534,7 @@ theorem isLocalization_stalk'
   rw [IsAffineOpen.fromSpec_app_self, Category.assoc, TopCat.Presheaf.germ_res]
   rfl
 
--- Porting note: I have splitted this into two lemmas
+-- Porting note: I have split this into two lemmas
 theorem isLocalization_stalk (x : U) :
     IsLocalization.AtPrime (X.presheaf.stalk x) (hU.primeIdealOf x).asIdeal := by
   rcases x with ⟨x, hx⟩