mathlib3

92ef3c51 - feat(ring_theory/graded_algebra/radical) : radical of homogeneous ideal is homogeneous (#12277)

feat(ring_theory/graded_algebra/radical) : radical of homogeneous ideal is homogeneous (#12277) This pr contains the following results about homogeneous ideals. * `ideal.is_homogeneous.is_prime_iff`: for any `I : ideal A`, if `I` is homogeneous, then `I` is prime if and only if `I` is homogeneously prime, i.e. `I ≠ ⊤` and if `x, y` are homogeneous elements such that `x * y ∈ I`, then at least one of `x,y` is in `I`. * `ideal.is_prime.homogeneous_core`: for any `I : ideal A`, if `I` is prime, then `I.homogeneous_core 𝒜` (i.e. the largest homogeneous ideal contained in `I`) is also prime. * `ideal.is_homogeneous.radical`: for any `I : ideal A`, if `I` is homogeneous, then the radical of `I` is homogeneous as well. * `homogeneous_ideal.radical`: for any `I : homogeneous_ideal 𝒜`, `I.radical` is the the radical of `I` as a `homogeneous_ideal 𝒜` Co-authored-by: Eric Wieser <wieser.eric@gmail.com>