Theorem CommRingCat.epi_iff_tmul_eq_tmul

Modification history

2024-11-06 15:34
Mathlib/Algebra/Category/Ring/Epi.lean
feat(Algebra/Category): for ring homs, epi + finite => surjective (#18267)
Added CommRingCat.epi_iff_tmul_eq_tmulView on Github →