Mathlib v3 is deprecated. Go to Mathlib v4

Def Module.unique_of_epi_zero

Modification history

2022-03-04 21:44
src/algebra/category/Module/epi_mono.lean
feat(ring_theory/simple_module): Simple modules as simple objects in the Module category (#11927) …
Added Module.unique_of_epi_zeroView on Github →