Theorem Submodule.IsPrimary.radical_colon_singleton_eq_ite

Modification history

2026-02-21 11:43
Mathlib/RingTheory/IsPrimary.lean
feat(RingTheory/Lasker): prove first uniqueness theorem for primary decomposition (#34699) …
Added Submodule.IsPrimary.radical_colon_singleton_eq_iteView on Github →