Commit 2025-02-10 17:54 bec437b2

View on Github →

feat(RingTheory/GradedAlgebra): define homogeneous submodule (#18728) and redefine homogeneous ideal as a homogeneous submodule rename SetLike.Homogeneous to SetLike.IsHomogeneousElem introduced DirectSum.SetLike.Homogeneous to mean a set $S$ is homogeneous iff for all $s \in S$, all of its projection $s_i \in S$ as well.

Estimated changes

deleted def SetLike.Homogeneous
deleted theorem SetLike.homogeneous_coe
deleted theorem SetLike.homogeneous_mul
deleted theorem SetLike.homogeneous_one
deleted structure HomogeneousIdeal
deleted def Ideal.IsHomogeneous
modified theorem Ideal.homogeneous_span
added structure HomogeneousSubmodule