Commit 2023-04-13 11:38 e3039685

View on Github →

feat: port Algebra.Category.Module.EpiMono (#3413)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

added theorem ModuleCat.epi_iff_range_eq_top

added theorem ModuleCat.epi_iff_surjective

added theorem ModuleCat.ker_eq_bot_of_mono

added theorem ModuleCat.mono_iff_injective

added theorem ModuleCat.mono_iff_ker_eq_bot

added theorem ModuleCat.range_eq_top_of_epi

added def ModuleCat.uniqueOfEpiZero