Theorem Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite

Modification history

2026-03-04 10:55
Mathlib/RingTheory/Lasker.lean
feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition (#35599) …
Added Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iteView on Github →