Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-06-27 11:16
4daf382a
View on Github →
feat(RingTheory/GradedAlgebra/Noetherian): properties of a graded Noetherian ring (
#8187
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/DirectSum/Internal.lean
added
theorem
SetLike.GradeZero.coe_algebraMap
added
theorem
SetLike.GradeZero.coe_intCast
added
theorem
SetLike.GradeZero.coe_natCast
added
theorem
SetLike.GradeZero.coe_ofNat
added
def
SetLike.GradeZero.subalgebra
added
def
SetLike.GradeZero.subring
added
def
SetLike.GradeZero.subsemiring
Modified
Mathlib/Algebra/GradedMonoid.lean
added
theorem
SetLike.GradeZero.coe_mul
added
theorem
SetLike.GradeZero.coe_one
added
theorem
SetLike.GradeZero.coe_pow
added
def
SetLike.GradeZero.submonoid
Modified
Mathlib/RingTheory/GradedAlgebra/Basic.lean
added
theorem
GradedRing.coe_projZeroRingHom'_apply
added
def
GradedRing.projZeroRingHom'
added
theorem
GradedRing.projZeroRingHom'_apply_coe
added
theorem
GradedRing.projZeroRingHom'_surjective
Created
Mathlib/RingTheory/GradedAlgebra/Noetherian.lean