Structure Submodule.IsMinimalPrimaryDecomposition

Modification history

2026-02-01 08:04

Mathlib/RingTheory/Lasker.lean

refactor(RingTheory/Lasker): generalize from `Ideal` to `Submodule` (#34135) …

Added Submodule.IsMinimalPrimaryDecomposition View on Github →