Commit 2022-03-12 04:22 6ee6203c

feat(counterexample) : a homogeneous ideal that is not prime but homogeneously prime (#12485) For graded rings, if the indexing set is nice, then a homogeneous ideal I is prime if and only if it is homogeneously prime, i.e. product of two homogeneous elements being in I implying at least one of them is in I. This fact is in src/ring_theory/graded_algebra/radical.lean. This counter example is meant to show that "nice condition" at least needs to include cancellation property by exhibiting an ideal in Zmod4^2 graded by a two element set being homogeneously prime but not prime. In #12277, Eric suggests that this counter example is worth pr-ing, so here is the pr.