Kernel_of_Ring_Homomorphism_is_Ideal

Proved

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

ideal-theoryproofwikiring-homomorphisms

Let $\phi: \struct {R_1, +_1, \circ_1} \to \struct {R_2, +_2, \circ_2}$ be a ring homomorphism. Then the kernel of $\phi$ is an ideal of $R_1$ .

Preamble

import Mathlib.RingTheory.Ideal.Basic

Formal statement

theorem Kernel_of_Ring_Homomorphism_is_Ideal {R₁ R₂ : Type _} [CommRing R₁] [CommRing R₂] (f : R₁ →+* R₂) : ∃ I : Ideal R₁, (↑I : Set R₁) = {x | f x = 0} := by sorry

Source

https://proofwiki.org/wiki/Kernel_of_Ring_Homomorphism_is_Ideal

View graph