Quotient_Ring_of_Kernel_of_Ring_Epimorphism
Provedproofwikiquotient-ringsring-epimorphismsring-isomorphisms
Let be a ring epimorphism. Let . Then there is a unique ring isomorphism such that is an isomorphism .
Preamble
import Mathlib.RingTheory.Ideal.Quotient.Basic import Mathlib.RingTheory.Ideal.Quotient.Operations
Formal statement
theorem Quotient_Ring_of_Kernel_of_Ring_Epimorphism {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : RingHom R₁ R₂) (hf : Function.Surjective f) : ∃ g : R₁ ⧸ RingHom.ker f →+* R₂, Function.Bijective g := by sorrySource