Commit 2025-11-17 16:19 b6ead3df

View on Github →

feat(RingTheory): some lemmas about the irrelevant ideal (#30336) This PR adds some lemmas about the irrelevant ideal of a graded ring, such as the fact that it is the iSup of each positively graded component.

Estimated changes

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

modified def HomogeneousIdeal.irrelevant

added theorem HomogeneousIdeal.irrelevant_eq_closure

added theorem HomogeneousIdeal.irrelevant_eq_iSup

added theorem HomogeneousIdeal.irrelevant_eq_span

added theorem HomogeneousIdeal.irrelevant_le

modified theorem HomogeneousIdeal.mem_irrelevant_iff

added theorem HomogeneousIdeal.mem_irrelevant_of_mem

added theorem HomogeneousIdeal.toAddSubmonoid_irrelevant_le

modified theorem HomogeneousIdeal.toIdeal_irrelevant

added theorem HomogeneousIdeal.toIdeal_irrelevant_le