Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-15 10:32 d199eb99

View on Github →

feat(ring_theory/graded_algebra/homogeneous_ideal): refactor homogeneous_ideal as a structure extending ideals (#12673) We refactored homogeneous_ideal as a structure extending ideals so that we can define a set_like (homogeneous_ideal \McA) A instance.

Estimated changes

deleted theorem homogeneous_ideal.coe_Inf
deleted theorem homogeneous_ideal.coe_Sup
deleted theorem homogeneous_ideal.coe_add
deleted theorem homogeneous_ideal.coe_bot
deleted theorem homogeneous_ideal.coe_inf
deleted theorem homogeneous_ideal.coe_mul
deleted theorem homogeneous_ideal.coe_sup
deleted theorem homogeneous_ideal.coe_top
added theorem homogeneous_ideal.ext
added structure homogeneous_ideal
deleted def homogeneous_ideal
modified theorem ideal.homogeneous_core.gc
modified theorem ideal.homogeneous_hull.gc
modified theorem ideal.is_homogeneous.iff_eq