feat: first isomorphism theorem for rings (#7536)

This matches the textbook version which does not assume surjectivity, and is also consistent with the Mathlib group theory version.

Mathlib/RingTheory/Ideal/Operations.lean

@@ -2105,6 +2105,10 @@ variable {F : Type*} [Ring R] [Ring S] [rc : RingHomClass F R S] (f : F)
 theorem sub_mem_ker_iff {x y} : x - y ∈ ker f ↔ f x = f y := by rw [mem_ker, map_sub, sub_eq_zero]
 #align ring_hom.sub_mem_ker_iff RingHom.sub_mem_ker_iff
 
+@[simp]
+theorem ker_rangeRestrict (f : R →+* S) : ker f.rangeRestrict = ker f :=
+  Ideal.ext fun _ ↦ Subtype.ext_iff
+
 end RingRing
 
 /-- The kernel of a homomorphism to a domain is a prime ideal. -/

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -76,11 +76,16 @@ theorem quotientKerEquivOfRightInverse.Symm.apply {g : S → R} (hf : Function.R
   rfl
 #align ring_hom.quotient_ker_equiv_of_right_inverse.symm.apply RingHom.quotientKerEquivOfRightInverse.Symm.apply
 
-/-- The **first isomorphism theorem** for commutative rings. -/
+/-- The **first isomorphism theorem** for commutative rings, surjective case. -/
 noncomputable def quotientKerEquivOfSurjective (hf : Function.Surjective f) : R ⧸ (ker f) ≃+* S :=
   quotientKerEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)
 #align ring_hom.quotient_ker_equiv_of_surjective RingHom.quotientKerEquivOfSurjective
 
+/-- The **first isomorphism theorem** for commutative rings. -/
+noncomputable def quotientKerEquivRange (f : R →+* S) : R ⧸ ker f ≃+* f.range :=
+  (Ideal.quotEquivOfEq f.ker_rangeRestrict.symm).trans <|
+    quotientKerEquivOfSurjective f.rangeRestrict_surjective
+
 end RingHom
 
 namespace Ideal