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