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