Skip to content

Commit

Permalink
fix(counterexamples): typo in module docstring (#13378)
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin committed Apr 12, 2022
1 parent 36bafae commit 9984960
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion counterexamples/homogeneous_prime_not_prime.lean
Expand Up @@ -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
Expand Down

0 comments on commit 9984960

Please sign in to comment.