Ring_Epimorphism_with_Trivial_Kernel_is_Isomorphism

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiring-epimorphismsring-isomorphisms

Let $\phi: \left({R_1, +_1, \circ_1}\right) \to \left({R_2, +_2, \circ_2}\right)$ be a ring epimorphism. Then $\phi$ is a ring isomorphism iff $\ker \left({\phi}\right) = \left\{ {0_{R_1} }\right\}$ .

Preamble

import Mathlib.RingTheory.Ideal.Quotient.Basic

Formal statement

theorem Ring_Epimorphism_with_Trivial_Kernel_is_Isomorphism {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : R₁ →+* R₂) (hf : Function.Surjective f) : Function.Injective f ↔ (∀ x, f x = 0 → x = 0) := by sorry

Source

https://proofwiki.org/wiki/Ring_Epimorphism_with_Trivial_Kernel_is_Isomorphism

View graph