diff --git a/counterexamples/homogeneous_prime_not_prime.lean b/counterexamples/homogeneous_prime_not_prime.lean
index b448e26a8848c..0374a5f9d06c0 100644
--- a/counterexamples/homogeneous_prime_not_prime.lean
+++ b/counterexamples/homogeneous_prime_not_prime.lean
@@ -10,7 +10,7 @@ import tactic.derive_fintype
 /-!
 # A homogeneous prime that is homogeneously prime but not prime
 
-In `src/ring_theory/graded_algebra/radical.lean`,  we assumed that the underline grading is inedxed
+In `src/ring_theory/graded_algebra/radical.lean`,  we assumed that the underline grading is indexed
 by a `linear_ordered_cancel_add_comm_monoid` to prove that a homogeneous ideal is prime if and only
 if it is homogeneously prime. This file is aimed to show that even if this assumption isn't strictly
 necessary, the assumption of "being cancellative" is. We construct a counterexample where the