mathlib3

6ee6203c - feat(counterexample) : a homogeneous ideal that is not prime but homogeneously prime (#12485)

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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>