Commit 2024-11-06 15:34 a78ac3bf

View on Github →

feat(Algebra/Category): for ring homs, epi + finite => surjective (#18267)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/Ring/Epi.lean

added theorem CommRingCat.epi_iff_tmul_eq_tmul

added theorem RingHom.surjective_iff_epi_and_finite

added theorem RingHom.surjective_of_epi_of_finite

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.exists_isPrincipal_quotient_of_finite

added theorem Module.exists_surjective_quotient_of_finite

Modified Mathlib/RingTheory/Ideal/IsPrincipal.lean

Modified Mathlib/RingTheory/TensorProduct/Finite.lean

added theorem RingHom.surjective_of_tmul_eq_tmul_of_finite