Theorems · Definition · ring theory
TwoSidedIdeal.ker
{R : Type u_1} →
{S : Type u_2} →
[inst : NonUnitalNonAssocRing R] →
[inst_1 : NonUnitalNonAssocSemiring S] →
{F : Type u_3} → [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → TwoSidedIdeal RThe kernel of a ring homomorphism, as a two-sided ideal.
- Defined in
- Mathlib.RingTheory.TwoSidedIdeal.Kernel
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- FunLikestatement and proof · cited by 2,560
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- NonUnitalNonAssocRingstatement and proof · cited by 354
- TwoSidedIdealstatement · cited by 151
- NonUnitalRingHomClassstatement and proof · cited by 82
Cited by6
Results whose statement or proof uses this declaration.
- IsSimpleRing.injective_ringHom_or_subsingleton_codomainproof · cited by 2
- TwoSidedIdeal.ker_eq_botstatement and proof · cited by 2
- TwoSidedIdeal.mem_kerstatement and proof · cited by 1
- TwoSidedIdeal.ker_ringConstatement · cited by 1
- TwoSidedIdeal.ker_ringCon_mk'statement and proof · cited by 1
- TwoSidedIdeal.ker.congr_simpstatement and proof · cited by 0