Theorem isSimpleModule_iff_isSimpleModule_of_algebraMap_surjective

Modification history

2026-04-14 10:54
Mathlib/RingTheory/SimpleModule/Basic.lean
feat(RingTheory): Order of vanishing in a discrete valuation ring (#29550) …
Added isSimpleModule_iff_isSimpleModule_of_algebraMap_surjectiveView on Github →