Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-10-27 13:11
62649052
View on Github →
feat(RingTheory/Lasker): decomposition into primary ideals (
#17123
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/RingTheory/Lasker.lean
added
theorem
Ideal.exists_isPrimary_decomposition
added
theorem
Ideal.isLasker
added
theorem
InfIrred.isPrimary
added
def
IsLasker