Theorem InfIrred.isPrimary

Modification history

2024-10-27 13:11

Mathlib/RingTheory/Lasker.lean

feat(RingTheory/Lasker): decomposition into primary ideals (#17123)

Added InfIrred.isPrimary View on Github →