Theorem Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul

Modification history

2024-10-28 20:08
Mathlib/RingTheory/IsPrimary.lean
feat(RingTheory): generalize `Ideal.IsPrimary` to submodules (#17073) …
Added Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smulView on Github →