Documentation

Mathlib.RingTheory.TwoSidedIdeal.Kernel

Kernel of a ring homomorphism as a two-sided ideal #

In this file we define the kernel of a ring homomorphism f : R → S as a two-sided ideal of R.

We put this in a separate file so that we could import it in SimpleRing/Basic.lean without importing any finiteness result.

The kernel of a ring homomorphism, as a two-sided ideal.

Equations
Instances For
    @[simp]
    theorem TwoSidedIdeal.ker_ringCon {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x y : R} :
    (ker f).ringCon x y f x = f y
    theorem TwoSidedIdeal.mem_ker {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocRing R] [NonUnitalNonAssocSemiring S] {F : Type u_3} [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R} :
    @[simp]

    The kernel of the ring homomorphism R → R⧸I is I.